fact: Definition map_option (A B:Type) (f : A -> option B) (o : option A) : option B := match o with | None => None | Some x => f x end.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl