proposition: Lemma mem_inv_middle_first : forall l x, mem x l -> exists l1 l2, l = l1++x::l2 /\ ~ mem x l1.
proof: Proof. Proof using. introv M. induction M. { exists (@nil A) l. rewrite* mem_nil_eq. } { tests C: (x=y). { exists (@nil A) l. rewrite* mem_nil_eq. } { destruct IHM as (l1&l2&E&N). exists (y::l1) l2. subst. rew_list. rewrite* mem_cons_eq. } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)