proposition: Lemma pair_extensionality : forall a b, is_pair a -> is_pair b -> pr1 a = pr1 b -> pr2 a = pr2 b -> a = b.
proof: Proof. ir. transitivity (pair (pr1 a) (pr2 a)). assert (pair_recovers a). app pair_recov. uh H3. sy; am. rw H1; rw H2. assert (pair_recovers b). app pair_recov. uh H3. am. Qed.
imports: tactics