proposition: Lemma Map_resp_StepF_eq: forall f:X-->Y, (forall x y, (st_eq x y)-> (st_eq (f x) (f y))) -> forall s t:(StepF X), s == t -> (f ^@> s) == (f ^@> t).
proof: Proof. intros f H. induction s. induction t. unfold StepF_eq, Map2, StepFfoldProp ;simpl;auto with *. unfold StepF_eq, Map2, StepFfoldProp. simpl; intuition. intros t H0. unfold StepF_eq, Map2 in H0. rewrite MapGlue in H0. rewrite ApGlue in H0. unfold StepF_eq, Map2. repeat rewrite MapGlue. rewrite ApGlue. rewrite SplitLMap. rewrite SplitRMap. destruct H0 as [H0l H0R]. split. apply IHs1; auto. apply IHs2; 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