proposition: Lemma StepF_eq_resp_Qeq : forall (s t : StepF X) u v, (StepF_Qeq s t) -> (StepF_Qeq u v) -> s == u -> t == v.
proof: Proof. induction s; induction t; try contradiction. intros u v Hst Huv Hsu. simpl in Hst. unfold StepF_eq in *. rewrite <- Hst. rewrite <- (StepFfoldProp_morphism ((st_eqS) ^@> constStepF x <@> u)); auto. apply: (Map_resp_StepF_eq); auto with *. intros a b Hab. simpl. rewrite -> Hab. reflexivity. intros u v [H [Hst0 Hst1]] Huv Hsu. destruct Hsu as [Hsu1 Hsu2] using (glue_eq_ind s1). apply glue_StepF_eq. eapply IHs1. assumption. unfold SplitL; apply SplitL_resp_Qeq. apply H. apply Huv. assumption. eapply IHs2. assumption. unfold SplitR; apply SplitR_resp_Qeq. apply H. apply Huv. 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