dsimp [dfold]
case succ
α : Nat → Sort u
β : Nat → Sort v
f : (n : Nat) → α n → β n
g₁ : (n : Nat) → α n → α (n + 1)
g₂ : (n : Nat) → β n → β (n + 1)
init : α 0
H : ∀ (n : Nat) (a : α n), g₂ n (f n a) = f (n + 1) (g₁ n a)
n : Nat
IH : dfold g₂ n (f 0 init) = f n (dfold g₁ n init)
⊢ dfold g₂ (succ n) (f 0 init) = f (succ n) (dfold g₁ (succ n) init)
case succ
α : Nat → Sort u
β : Nat → Sort v
f : (n : Nat) → α n → β n
g₁ : (n : Nat) → α n → α (n + 1)
g₂ : (n : Nat) → β n → β (n + 1)
init : α 0
H : ∀ (n : Nat) (a : α n), g₂ n (f n a) = f (n + 1) (g₁ n a)
n : Nat
IH : dfold g₂ n (f 0 init) = f n (dfold g₁ n init)
⊢ g₂ n (dfold g₂ n (f 0 init)) = f (succ n) (g₁ n (dfold g₁ n init))