proposition: Lemma mem_impl_in : (forall a b, eqA a b -> a = b) -> forall e l, mem e l -> In e l.
proof: Proof. fix mem_impl_in 3. intros eq_is_eq e l; case l; clear l. intro e_mem_nil; contradiction. simpl; intros a l [e_eq_a | e_mem_l]. left; symmetry; apply eq_is_eq; assumption. right; apply mem_impl_in; assumption. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)