rintro rfl
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 : ℕ
w₁ : WType β
h₁ : w₁.depth ≤ s
w₂ : WType β
h₂ : w₂.depth ≤ s
⊢ w₁ = w₂ → ⟨w₁, h₁⟩ = ⟨w₂, 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 : ℕ
w₁ : WType β
h₁ h₂ : w₁.depth ≤ s
⊢ ⟨w₁, h₁⟩ = ⟨w₁, h₂⟩