proposition: Lemma union2_or : forall x y a : E, inc a (union2 x y) -> inc a x \/ inc a y.
proof: Proof. ir. unfold union2 in H. pose (union_exists H). nin e. xd. pose (doubleton_or H1). nin o. rewrite H2 in H0. intuition. rewrite H2 in H0; intuition. Qed.
imports: tactics