proposition: Lemma inter_2 : forall s1 s2 e, mem e (inter s1 s2) -> mem e s2.
proof: Proof. intros [l1 wr1] [l2 wr2] e H; simpl. generalize (inter_2_aux nil l1 l2 e H). intros [ H' | H']; trivial; contradiction. Qed.
imports: List more_list list_permut Arith