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