proposition: Lemma bind_terminates_l: forall (A: Type) (m: delay A) (v: A), terminates m v -> forall (B: Type) (f: A -> delay B), bind m f == f v.
proof: Proof. induction 1; intros. - apply mon_law_1. - rewrite bind_later. eapply equi_trans. apply eq_later. apply IHterminates. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP)