proposition: Lemma StepFfoldPropForall_Map2 : forall X Y (f:X --> Y --> iffSetoid) x y, (forall a b, f a b) -> StepFfoldProp (f ^@> x <@> y).
proof: Proof. intros X Y f x y H. apply StepFfoldPropForall_Ap. intros b. rewrite <- (Map_commutative (constStepF f) (constStepF b)). rewriteStepF. apply StepFfoldPropForall_Map. intros a. apply: H. 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