proposition: Lemma intersection2_first : forall x y a : E, inc a (intersection2 x y) -> inc a x.
proof: Proof. ir. unfold intersection2 in H. eapply intersection_forall with (doubleton x y). am. ap doubleton_first. Qed.
imports: tactics