proposition: Lemma SplitRGlue : forall x y:StepF, forall o, (SplitR (glue o x y) o)=y.
proof: Proof. unfold SplitR. intros. rewrite SplitGlue. reflexivity. Qed.
imports: CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.tactics.Qauto CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields