proposition: Lemma glueSplit : forall {X : RSetoid} (s : StepF X), forall a, (glue a (SplitL s a) (SplitR s a)) === s.
proof: Proof. intros X s a. apply glue_StepF_eq; 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