example.idr

ones : List Nat -> List Nat
ones = map (const 1)

f : (input:List Nat) -> (sum (ones input) = length input)
f input = case input of
               [] => Refl
               (x::xs) => ?hole

Ok, so List is recursive, and you usually prove stuff about such types also in a recursive manner. You've done the corner case of [], now you prove by induction (basically a dependent version of recursion) - assume f xs and use it to prove f (x :: xs) somehow. Try writing let fx = f xs in ?hole.