proposition: Lemma Map_discardable (X Y : RSetoid) : forall (a:StepF X) (b:StepF Y), ((@const _ _) ^@> a <@> b == a).
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. 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