proposition: Lemma Ap_interchange (X Y : RSetoid) : forall (f:StepF (X-->Y)) (a:X), (f <@^ a) == (flip id a) ^@> f.
proof: Proof. intros f a. 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