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