proposition: Lemma mem_concat_eq : forall m x, mem x (concat m) = exists l, mem l m /\ mem x l.
proof: Proof. Proof using. Hint Constructors mem. introv. extens. induction m. { simpl. iff I. { inverts I. } { destruct I as (?&H&?). inverts H. } } { rewrite concat_cons. rewrite mem_app_eq. iff I (l&M&N). { destruct I as [I|I]. { exists~ a. } { rewrite IHm in I. destruct* I as (l&?&?). } } { inverts* M. } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)