proposition: Remark bind_mono: forall (A B: Type) (x x': option A) (f f': A -> option B), x <<= x' -> (forall v, f v <<= f' v) -> bind x f <<= bind x' f'.
proof: Proof. intros. destruct H; cbn; auto with lessdef. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP Compil) Coq(Classical Description)