proposition: Lemma StFBind_wd(X Y : RSetoid): forall x1 x2 : StepFS X, st_eq x1 x2 -> st_eq (StFBind1 Y x1) (StFBind1 Y x2).
proof: Proof. induction x1. intro y. induction y. simpl. intro H. intro f. apply f. exact H. simpl. intro H. destruct H as [Hl Hr] using (eq_glue_ind y1). intro f. rewrite <- (IHy1 Hl (compose1 (SplitLS Y o) f)). simpl. unfold compose0. clear IHy1. rewrite <- (IHy2 Hr (compose1 (SplitRS Y o) f)). simpl. unfold compose0. unfold SplitLS0, SplitRS0. symmetry. apply: @glueSplit. intros y H f. simpl in H. destruct H as [Hl Hr] using (glue_eq_ind x1_1). simpl. rewrite -> (IHx1_1 _ Hl (compose1 (SplitLS Y o) f)). rewrite -> (IHx1_2 _ Hr (compose1 (SplitRS Y o) f)). clear IHx1_1 IHx1_2. change ((StFBind1 _ (glue o (SplitL y o) (SplitR y o)) f) == StFBind00 y f). clear Hl Hr x1_1 x1_2. simpl. rewrite <- (glueSplit (StFBind00 y f) o). rewrite -> SplitLBind. rewrite -> SplitRBind. reflexivity. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.StepFunctionSetoid CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.logic.CornBasics