proposition: Lemma mon_law_3: forall (A B C: Type) (m: delay A) (f: A -> delay B) (g: B -> delay C), bind (bind m f) g == bind m (fun x => bind (f x) g).
proof: Proof. cofix CIH. intros; destruct m. - rewrite ! bind_now, bind_later. apply equi_refl. - rewrite ! bind_later. constructor. apply CIH. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP)