proposition: Lemma pair_recov : forall u : E, is_pair u -> pair_recovers u.
proof: Proof. ir. unfold is_pair in H. unfold pair_recovers in |- *. pose (choose_pr H). assert (ex (fun y : E => ex (fun x : E => u = pair x y))). nin e. apply ex_intro with x. apply ex_intro with (pr1 u). am. pose (choose_pr H0). nin e. nin e0. assert (u = pair (pr1 u) x). am. assert (u = pair x0 (pr2 u)). am. assert (pair (pr1 u) x = pair x0 (pr2 u)). rewrite <- H3. am. pose (lem1 H5). rewrite e. sy. am. Qed.
imports: tactics