proposition: Lemma mem_induct : forall (x : A) (P : list A -> Prop), (forall l : list A, P (x :: l)) -> (forall (y : A) (l : list A), mem x l -> x <> y -> P l -> P (y :: l)) -> (forall l : list A, mem x l -> P l).
proof: Proof. Proof using. introv HH HN M. induction l. inverts M. tests: (x = a). auto. inverts M; auto_false*. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)