proposition: Lemma u_mon: forall {A: Type} (x: mon A), x = match x with Ret v => Ret v | Bind y f => Bind y f | Later m => Later m end.
proof: Proof. destruct x; auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP)