proposition: Lemma eq_list_of_not_mem : forall l, (forall x, ~ mem x l) -> l = nil.
proof: Proof. Proof using. introv P. destruct~ l. false P. applys mem_here. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)