simp at h
case mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s₁ s₂ : ℕ
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
w✝ : WType β
hw₁ : w✝.depth ≤ s₁
w : WType β
hw₂ : w.depth ≤ s₂
h : ↑⟨w✝, hw₁⟩ = ↑⟨w, hw₂⟩
⊢ elim' γ fγ s₁ ⟨w✝, hw₁⟩ = elim' γ fγ s₂ ⟨w, hw₂⟩
case mk.mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s₁ s₂ : ℕ
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
w✝ : WType β
hw₁ : w✝.depth ≤ s₁
w : WType β
hw₂ : w.depth ≤ s₂
h : w✝ = w
⊢ elim' γ fγ s₁ ⟨w✝, hw₁⟩ = elim' γ fγ s₂ ⟨w, hw₂⟩