pub proof fn entails_and_equality<T>(p: TempPred<T>, q: TempPred<T>)
p.entails(q),
p == p.and(q),
Make the predicate as concise as possible.
Similar to the first-order logic where p equals p ∧ q when p -> q is satisfied, we can reduce the size of predicate when some part of it implies the rest.
p
p ∧ q
p -> q
p ⊧ q
p == p ∧ q