proposition: Lemma length_map : forall f l, length (map f l) = length l.
proof: Proof. Proof using. intros. induction~ l. { rewrite map_cons. do 2 rewrite length_cons. auto. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)