proposition: Lemma lem2 : forall x y z w : E, pair x y = pair z w -> y = w.
proof: Proof. ir. assert (inc (doubleton emptyset (singleton y)) (pair z w)). rewrite <- H. unfold pair in |- *. ap doubleton_second. unfold pair in H0. pose (doubleton_or H0). nin o. assert (inc emptyset (singleton z)). rewrite <- H1. ap doubleton_first. assert (inc (singleton y) (singleton z)). rewrite <- H1. ap doubleton_second. pose (singleton_eq H2). pose (singleton_eq H3). assert (inc y emptyset). rewrite e. rewrite <- e0. ap singleton_inc. pose (emptyset_empty H4). elim f. assert (inc (singleton y) (doubleton emptyset (singleton w))). rewrite <- H1. ap doubleton_second. pose (doubleton_or H2). nin o. assert (inc y emptyset). rewrite <- H3. ap singleton_inc. pose (emptyset_empty H4). elim f. ap singleton_inj. am. Qed.
imports: tactics