proposition: Lemma ApBind(X Y : RSetoid): forall (x:(StepFS X)) (f:StepFS (X-->Y)) , (f<@>x== (@StFBind _ _ f (compose (StFBind _ _ x) (compose (StFReturn _))))).
proof: Proof. apply: StepF_ind2. intros s s0 t t0 Hs Ht H. rewrite <- Hs, <- Ht at 1. rewrite -> H. unfold StFBind. simpl. transitivity (StFBind00 t0 (compose1 (StFBind1 Y s) (compose2 X (StFReturn Y)))). apply: StFBind_wd; auto. apply StFBind_wd1. intros a. apply: StFBind_wd; auto. reflexivity. intros o s s0 t t0 IHf1 IHf2. rewrite ApGlueGlue. rewrite -> IHf1, IHf2. simpl. apply glue_wd; try reflexivity; apply StFBind_wd1; intro x; unfold StFBind1, compose1, compose0; simpl. unfold SplitLS0. rewrite SplitLGlue. apply StFBind_wd1. intro y. reflexivity. unfold SplitRS0. rewrite SplitRGlue. apply StFBind_wd1. intro y. reflexivity. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.StepFunctionSetoid CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.logic.CornBasics