Отверстие с задержкой в ​​типе. Как доказать?

Question

Я пытался доказать, что replicate1 работает правильно, показывая, что все элементы replicate1 n x равны x:

all1 : (p : a -> Bool) -> List a -> Bool
all1 p [] = True
all1 p (x :: xs) = p x && all1 p xs

replicate1 : (n: Nat) -> a -> List a
replicate1 Z x = [x]
replicate1 (S k) x = x :: replicate1 k x

all_replicate_is_x : Eq a => {x: a} -> all1 (== x) (replicate1 n x) = True
all_replicate_is_x {n = Z} = ?hole
all_replicate_is_x {n = (S k)} = ?all_replicate_is_x_rhs_2

Базовое отверстие корпуса

Test.hole [P]
 `--           a : Type
      constraint : Eq a
               x : a
     -----------------------------------------
      Test.hole : x == x && Delay True = True

Как это доказать?