proposition: Lemma elim_not_In_cons : forall (A : Type) (y : A) (ys : list A) (x : A), ~ In x (y :: ys) -> x <> y /\ ~ In x ys.
proof: Proof. simpl. intuition. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList Metalib.CoqUniquenessTac