proposition: Lemma intersection2_inc : forall x y a : E, inc a x -> inc a y -> inc a (intersection2 x y).
proof: Proof. ir. unfold intersection2 in |- *. ap intersection_inc. apply nonempty_intro with x. ap doubleton_first. ir. cp (doubleton_or H1). nin H2. rewrite H2. am. rewrite H2. am. Qed.
imports: tactics