proposition: Lemma concat_eq_nil_mem_inv : forall l m, concat m = nil -> mem l m -> l = nil.
proof: Proof. Proof using. introv E M. induction M as [|x]. { rewrite concat_cons in E. forwards*: app_eq_nil_inv E. } { rewrite concat_cons in E. destruct x. { rew_list in E. applys~ IHM. } { rew_list in E. false. } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)