proposition: Lemma StepF_Qeq_eq : forall {X : RSetoid} (s t:StepF X), (StepF_Qeq s t) -> s === t.
proof: Proof. intro X. induction s; induction t; try contradiction; simpl. intros H. rewrite H. auto with *. intros [H [H0 H1]]. apply glue_StepF_eq. apply IHs1. apply SplitL_glue_ind; intros H2; try (elim (Qlt_not_le _ _ H2); rewrite -> H); auto with *. apply IHs2. apply SplitR_glue_ind; intros H2; try (elim (Qlt_not_le _ _ H2); rewrite -> H); auto with *. 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