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