proposition: Lemma Map_copyable X Y : forall (f:StepF (X --> X --> Y)) (x:StepF X), ((@join _ _) ^@> f <@> x) == (f <@> x <@> x).
proof: Proof. apply StepF_ind2; auto with *. intros s s0 t t0 Hs Ht. rewrite -> Hs, Ht; auto. intros o s s0 t t0 H0 H1. rewrite MapGlue. do 3 rewrite ApGlueGlue. rewrite -> H0, H1;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