proposition: Lemma singles_def : singles = fun xs vs => fold_right (fun p acc => concat acc (single (fst p) (snd p))) empty (combine xs vs).
proof: Proof. Proof using. reflexivity. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)