proposition: Lemma run_Bind_aux: forall (A B C: Type) (m: mon A) (k: cont A B) (f: B -> mon C), run (Bind m (insert_cont k f)) == bind (run (Bind m (insert_cont k (@Ret _)))) (fun x => run (f x)).
proof: Proof. cofix CIH; intros. destruct m. - rewrite ! run_Bind_Ret. destruct k; cbn. + rewrite run_Ret, bind_later, bind_now. constructor. apply equi_sym; apply eq_later. + rewrite bind_later. apply equi_later. apply CIH. - rewrite ! run_Bind_Later, bind_later. apply equi_later. apply CIH. - rewrite ! run_Bind_Bind, bind_later. apply equi_later. apply CIH with (k := Kbind m0 k). Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP)