proposition: Lemma Map_composition (X Y Z : RSetoid) : forall (a:StepF (Y-->Z)) (b:StepF (X-->Y)) (c:StepF X), ((@compose X Y Z) ^@> a <@> b <@> c) == (a <@> (b <@> c)).
proof: Proof. induction a. simpl. apply (StepF_ind2 (X --> Y) X); auto with *. intros s s0 t t0 Hs Ht. rewrite -> Hs, Ht. auto. intros o s s0 t t0 H H0. rewrite -> Map_homomorphism. rewrite ApGlueGlue. do 2 rewrite MapGlue. rewrite ApGlueGlue. rewrite <- H. rewrite <- H0. reflexivity. intros b c. rewrite MapGlue. repeat rewrite ApGlue. apply glue_resp_StepF_eq. rewrite -> IHa1. rewrite -> SplitLAp. reflexivity. rewrite -> IHa2. rewrite -> SplitRAp. 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