proposition: Lemma StepFfoldPropForall_Ap : forall X (f:StepF (X --> iffSetoid)) (x:StepF X), (forall y, StepFfoldProp (f <@> constStepF y)) -> StepFfoldProp (f <@> x).
proof: Proof. intros X f x H. revert f H. induction x. intros f H. apply H. intros f H. rewrite <- (glueSplit f o). rewrite ApGlueGlue. split. apply IHx1. intros y. assert (H0:=H y). rewrite <- (glueSplit f o) in H0. rewrite ApGlue in H0. destruct H0 as [H0 _]. assumption. apply IHx2. intros y. assert (H0:=H y). rewrite <- (glueSplit f o) in H0. rewrite ApGlue in H0. destruct H0 as [_ H0]. assumption. 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