fact: Definition singles (xs : list var) (vs : list A) : env A := fold_right (fun p acc => concat acc (single (fst p) (snd p))) empty (combine xs vs).
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)