proposition: Lemma mon_law_2: forall (A: Type) (m: delay A), bind m (@ret A) == m.
proof: Proof. cofix CIH; intros. destruct m. - rewrite bind_now. apply eq_later. - rewrite bind_later. constructor. apply CIH. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP)