fact: Definition bind {A B: Type} (m: option A) (f: A -> option B) : option B := match m with None => None | Some s => f s end.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP Compil) Coq(Classical Description)