proposition: Lemma Map_ap X Y Z : forall (f:StepF (X --> Y --> Z)) (x:StepF (X --> Y)) (a:StepF X), ((@ap _ _ _) ^@> f <@> x <@> a) == (f <@> a <@> (x <@> a)).
proof: Proof. intros f x a. unfold ap. evalStepF. 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