proposition: Lemma Map_homomorphism : forall X Y (f:X->Y) (a:X), (f ^@> constStepF a) = (constStepF (f a)).
proof: Proof. exact Ap_homomorphism. Qed.
imports: CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields