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