proposition: Lemma StepF_eq_trans:forall x y z : StepF X, x == y -> y == z -> x == z.
proof: Proof. induction x. intros. unfold StepF_eq in *. set (A:=((st_eqS :X-->X-->iffSetoid) ^@> constStepF x)) in *. rewrite <- (StepFfoldProp_morphism (A <@> y)); auto with *. apply: (Map_resp_StepF_eq); auto with *. intros a b Hab. simpl. rewrite -> Hab. reflexivity. intros. destruct H using (glue_eq_ind x1). apply glue_StepF_eq. eapply IHx1. apply H. apply SplitL_resp_Xeq. assumption. eapply IHx2. apply H1. apply SplitR_resp_Xeq. 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