proposition: Lemma doubleton_inj : forall x y z w : E, doubleton x y = doubleton z w -> A (x = z) (y = w) \/ A (x = w) (y = z).
proof: Proof. ir. assert (inc x (doubleton z w)). rewrite <- H. ap doubleton_first. pose (doubleton_or H0). assert (inc y (doubleton z w)). rewrite <- H. ap doubleton_second. pose (doubleton_or H1). nin o. nin o0. assert (inc w (doubleton x y)). rewrite H. ap doubleton_second. pose (doubleton_or H4). nin o. ap or_introl. xd. rewrite H5. rewrite H2. am. ap or_introl. xd. ap or_introl. xd. nin o0. ap or_intror. xd. assert (inc z (doubleton x y)). rewrite H. ap doubleton_first. pose (doubleton_or H4). nin o. ap or_introl. xd. ap or_introl. xd. rewrite H5. rewrite H3. am. Qed.
imports: tactics