proposition: Lemma Map_commutative W X Y : forall (f:StepF (W --> X --> Y)) (x:StepF X) (w:StepF W), ((@flip _ _ _) ^@> f <@> x <@> w) == (f <@> w <@> x).
proof: Proof. induction f. simpl. 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 -> Map_homomorphism. do 2 rewrite MapGlue. do 2 rewrite ApGlueGlue. rewrite -> H0, H1; reflexivity. intros x w. rewrite MapGlue. do 4 rewrite ApGlue. apply glue_resp_StepF_eq; auto. 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