rcases w₁ with ⟨w, hw₁⟩
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s₁ s₂ : ℕ
w₁ : SubWType β s₁
w₂ : SubWType β s₂
h : ↑w₁ = ↑w₂
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
⊢ elim' γ fγ s₁ w₁ = elim' γ fγ s₂ w₂
case 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₂ : ℕ
w₂ : SubWType β s₂
γ : Type u_3
fγ : (a : α) × (β a → γ) → γ
w : WType β
hw₁ : w.depth ≤ s₁
h : ↑⟨w, hw₁⟩ = ↑w₂
⊢ elim' γ fγ s₁ ⟨w, hw₁⟩ = elim' γ fγ s₂ w₂