proposition: Lemma StFBind_wd1(X Y : RSetoid):forall m, forall x1 x2 : X --> StepFS Y, st_eq x1 x2 -> st_eq (StFBind00 m x1) (StFBind00 m x2).
proof: Proof. induction m. intros x1 x2 H. simpl; auto with *. apply H. intros x1 x2 H. simpl. apply glue_resp_StepF_eq. apply IHm1. intro. simpl. unfold compose0. apply SplitL_wd; auto with *. apply H. apply IHm2. intro. simpl. unfold compose0. apply SplitR_wd; auto with *. apply H. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.StepFunctionSetoid CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.logic.CornBasics