proposition: Lemma MirrorGlue : forall (X : RSetoid) (o : OpenUnit) (al ar : StepF X), Mirror (glue o al ar) = glue (OpenUnitDual o) (Mirror ar) (Mirror al).
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