proposition: Lemma StepF_eq_refl : forall {X : RSetoid} (x : StepF X), x === x.
proof: Proof. intro X. induction x. change (st_eq x x). reflexivity. apply glue_StepF_eq. simpl; rewrite SplitLGlue; assumption. simpl; rewrite SplitRGlue; 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