proposition: Lemma not_In_cons : forall (A : Type) (ys : list A) (x y : A), x <> y -> ~ In x ys -> ~ In x (y :: ys).
proof: Proof. unfold not. inversion 3; auto. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList Metalib.CoqUniquenessTac