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