isSingleton : Bool -> Type
isSingleton True = Nat
isSingleton False = List Nat 

mkSingle : (x:Bool) -> isSingleton x
mkSingle True = 0
mkSingle False = []

sum : (single : Bool) -> isSingleton single -> Nat
sum True x = x
sum False [] = 0
sum False (x::xs) = x + sum False xs

