如何使用Agda中N的归纳原理证明N的递归器的定义方程命题成立?

这是来自 Homotopy Type Theory 书以下是我所拥有的:

data ℕ : Set where
    zero : ℕ
    succ : ℕ → ℕ

iter : {C : Set} → C → (C → C) → ℕ → C
iter z f  zero    = z
iter z f (succ n) = f (iter z f n)

succℕ : {C : Set} → (ℕ → C → C) → ℕ × C → ℕ × C
succℕ f (n , x) = (succ n , f n x)

iterℕ : {C : Set} → C → (ℕ → C → C) → ℕ → ℕ × C
iterℕ z f = iter (zero , z) (succℕ f)

recℕ : {C : Set} → C → (ℕ → C → C) → ℕ → C
recℕ z f = _×_.proj₂ ∘ iterℕ z f

indℕ : {C : ℕ → Set} → C zero → ((n : ℕ) → C n → C (succ n)) → (n : ℕ) → C n
indℕ z f  zero    = z
indℕ z f (succ n) = f n (indℕ z f n)

recℕzfzero≡z : {C : Set} {z : C} {f : ℕ → C → C} → recℕ z f zero ≡ z
recℕzfzero≡z = refl

recℕzfsuccn≡fnrecℕzfn : {C : Set} {z : C} {f : ℕ → C → C} (n : ℕ) →
                        recℕ z f (succ n) ≡ f n (recℕ z f n)
recℕzfsuccn≡fnrecℕzfn = indℕ refl ?

我不知道如何证明 recℕ z f (succ n) ≡ f n (recℕ z f n) 。我需要证明:

(n : ℕ) → recℕ z f (succ n) ≡ f n (recℕ z f n)
        → recℕ z f (succ (succ n)) ≡ f (succ n) (recℕ z f (succ n))

在英语中,给定一个自然数 n 归纳假说证明了结果。

中缀运算符 _∘_ 是正常的功能组成。这个 _≡_ 和 _×_ 数据类型定义为:

data _≡_ {A : Set} : A → A → Set where
    refl : {x : A} → x ≡ x

record _×_ (A B : Set) : Set where
    constructor _,_
    field
        _×_.proj₁ : A
        _×_.proj₂ : B

我一直在想一个解决方案,但我想不出如何解决这个问题。