proposition: Lemma BindReturn(m:StepF X): (StFBind X X m (StFReturn X)) == m.
proof: Proof. unfold StFBind. induction m. simpl. auto with *. simpl. unfold StFBind00. simpl. apply glue_resp_StepF_eq. clear IHm2 m2. simpl in IHm1. assert (extEq (StepFS X) (StFReturn X) (compose1 (SplitLS X o) (StFReturn X))). intro. simpl. auto with *. pose (s:=Morphism_prf (StFBind1 X m1) (StFReturn X) (compose1 (SplitLS X o) (StFReturn X)) H). rewrite -> s in IHm1. clear s H. assumption. clear IHm1 m1. simpl in IHm2. assert (extEq (StepFS X) (StFReturn X) (compose1 (SplitRS X o) (StFReturn X))). intro; simpl; auto with *. pose (s:=Morphism_prf (StFBind1 X m2) (StFReturn X) (compose1 (SplitRS X o) (StFReturn X)) H). rewrite -> s in IHm2. clear s H. assumption. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.StepFunctionSetoid CoRN.model.structures.OpenUnit CoRN.tactics.CornTac CoRN.logic.CornBasics