proposition: Lemma not_mem_cons_inv : forall x y l, ~ mem x (y::l) -> x <> y /\ ~ mem x l.
proof: Proof. Proof using. introv M. split. { intro_subst. false* M. } { intros N. false* M. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)