proposition: Lemma MapGlue : forall (X Y : RSetoid) (f : (X --> Y)) (o : OpenUnit) (al ar : StepF X), f ^@> (glue o al ar) = glue o (f ^@> al) (f ^@> ar).
proof: Proof. 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