proposition: Lemma GlueAp : forall (X Y : RSetoid) (f : StepF (X --> Y)) (o : OpenUnit) (l r : StepF X), f <@> (glue o l r) == glue o ((SplitL f o) <@> l) ((SplitR f o) <@> r).
proof: Proof. intros X Y f o l r. set (A:= ((SplitL f o)<@>l)). set (B:= ((SplitR f o)<@>r)). rewrite <- (glueSplit f o). rewrite ApGlueGlue. reflexivity. 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