proposition: Lemma StepFfoldPropSplitR : forall (s : StepF iffSetoid) (a : OpenUnit), StepFfoldProp s -> StepFfoldProp (SplitR s a).
proof: Proof. intros s a H. rewrite <- (StepFfoldPropglue s a) in H. destruct H; auto. 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