proposition: Theorem map_cons : forall (A B : Type)(f : A -> B) a ls, map f (a :: ls) = (f a) :: (map f ls).
proof: Proof. intuition idtac. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia Coq.Classes.RelationClasses Coq.Classes.Morphisms