Not-working proof

-- Does not work (in any reasonable amount of time)

allHasCount : Vect n (a, Nat) -> Nat -> Bool
allHasCount []             n = True
allHasCount ((a, b) :: xs) n = b == n && allHasCount xs n

addCount : (a -> a -> a) -> (a, Nat) -> (a, Nat) -> (a, Nat)
addCount f (a, n) (b, m) = (f a b, n + m + 1)

foldrHomoByte : (a:Vect 5 (b,Nat)) -> (f:b -> b -> b) -> (p:allHasCount a 1 = True) -> toIntegerNat (snd (foldr1 (addCount f) a)) = 9
foldrHomoByte [(a,(S Z)),(b,(S Z)),(c,(S Z)),(d,(S Z)),(e,(S Z))] f p = refl

Working proof

-- Works

allHasCount : Vect n (a, Nat) -> Nat -> Bool
allHasCount []             n = True
allHasCount ((a, b) :: xs) n = b == n && allHasCount xs n

addCount : (a -> a -> a) -> (a, Nat) -> (a, Nat) -> (a, Nat)
addCount f (a, n) (b, m) = (f a b, n + m + 1)

foldrHomoByte : (a:Vect 4 (b,Nat)) -> (f:b -> b -> b) -> (p:allHasCount a 1 = True) -> toIntegerNat (snd (foldr1 (addCount f) a)) = 7
foldrHomoByte [(a,(S Z)),(b,(S Z)),(c,(S Z)),(d,(S Z))] e p = refl