proposition: Lemma BindBind(Z : RSetoid)(m:StepF X)(f:X-->StepFS Y)(g:Y-->StepFS Z): (StFBind Y Z (StFBind X Y m f) g) == (StFBind X Z m (Bind_compose f g)).
proof: Proof. revert f g. induction m. simpl. unfold compose0. simpl; auto with *. simpl. intros. apply glue_resp_StepF_eq. clear IHm2 m2. simpl in IHm1. rewrite -> (IHm1 (compose1 (SplitLS Y o) f) (compose1 (SplitLS Z o) g)). clear IHm1. apply StFBind_wd1. intro. simpl. unfold compose0. symmetry. apply: SplitLBind. clear IHm1 m1. simpl in IHm2. rewrite -> (IHm2 (compose1 (SplitRS Y o) f) (compose1 (SplitRS Z o) g)). clear IHm2. apply StFBind_wd1. intro. simpl. unfold compose0. symmetry. apply: SplitRBind. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.StepFunctionSetoid CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.logic.CornBasics