proposition: Lemma eq_glue_ind {X : RSetoid} : forall (s1 s2 s : StepF X) (a : OpenUnit) (P : Prop), ((SplitL s a) == s1 -> (SplitR s a) == s2 -> P) -> s == (glue a s1 s2) -> P.
proof: Proof. intros s1 s2 s a P H H0. symmetry in H0. destruct H0 as [H0l H0r] using (glue_eq_ind s1). symmetry in H0l, H0r. auto. 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