proposition: Lemma StepFfoldProp_morphism:forall x y:(StepF iffSetoid), (StepF_eq x y) -> ((StepFfoldProp x)<->(StepFfoldProp y)).
proof: Proof. induction x. induction y. auto with *. unfold StepF_eq. simpl. unfold StepFfoldProp;simpl;intuition. intros y H0. unfold StepF_eq, Map2 in H0. rewrite MapGlue in H0. rewrite ApGlue in H0. destruct H0 as [H0l H0r]. change ((StepFfoldProp x1 /\ StepFfoldProp x2) <-> StepFfoldProp y). rewrite -> (IHx1 (SplitL y o)); auto with *. rewrite -> (IHx2 (SplitR y o)); auto with *. apply: StepFfoldPropglue. 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