exact this.allEq _ _
case a
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : σ → α
h : ∀ (x : σ), Fintype.card (β (f x)) = 1
hf : Primrec f
this✝ : Primrec₂ fun x w => (w.depth + 1).pair ((encode (f x)).pair (encode [(encode w).unpair.2]))
x : σ
w : WType β
this : Subsingleton (β (f x))
a✝ : β (f x)
⊢ a✝ = fintypeEquivFin.symm 0
no goals