proposition: Lemma map_id_ext : forall A (l:list A) (f:A->A), (forall x, f x = x) -> map f l = l.
proof: Proof. Proof using. introv E. cuts_rewrite (f = id). apply map_id. extens~. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)