proposition: Lemma inter_12 : forall s1 s2 e, mem e s1 -> mem e s2 -> mem e (inter s1 s2).
proof: Proof. intros [l1 wr1] [l2 wr2] e e_in_l1 e_in_l2; refine (inter_12_aux nil l1 l2 e _ _); trivial. Qed.
imports: List more_list list_permut Arith