proposition: Lemma MirrorBind(X Y : RSetoid):forall (x:StepF X) (f:X --> (StepFS Y)), Mirror (StFBind00 x f)==(StFBind00 (Mirror x) (compose (MirrorS Y) f)).
proof: Proof. induction x. reflexivity. intros. simpl. rewrite MirrorGlue. apply glue_wd; auto with *. rewrite -> IHx2. simpl. change (StFBind00 (Mirror x2) (compose1 (MirrorS Y) (compose1 (SplitRS Y o) f)) == StFBind00 (Mirror x2) (compose1 (SplitLS Y (OpenUnitDual o)) (compose1 (MirrorS Y) f))). apply StFBind_wd1. intro. simpl. unfold compose0. unfold SplitRS0, SplitLS0. apply MirrorSplitR; auto with *. rewrite -> IHx1. simpl. change (StFBind00 (Mirror x1) (compose1 (MirrorS Y) (compose1 (SplitLS Y o) f)) == StFBind00 (Mirror x1) (compose1 (SplitRS Y (OpenUnitDual o)) (compose1 (MirrorS Y) f))). apply StFBind_wd1. intro. simpl. unfold compose0. unfold SplitRS0, SplitLS0. apply MirrorSplitL; auto with *. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.StepFunctionSetoid CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.logic.CornBasics