proposition: Lemma map_eq_nil_inv : forall f l, map f l = nil -> l = nil.
proof: Proof. Proof using. introv E. destruct~ l. rewrite map_cons in E. false. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)