congr
α : Type u_1
β : α → Type u_2
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
γ : Type u_3
w : WType fun a => β a
inst✝ : Inhabited γ
f : (a : α) × (β a → γ) → γ
⊢ elim γ f w = elim γ (fun x => f ⟨x.fst, fintypeArrowEquivFinArrow.symm fun i => x.snd (fintypeEquivFin.symm i)⟩) w
case e_fγ
α : Type u_1
β : α → Type u_2
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
γ : Type u_3
w : WType fun a => β a
inst✝ : Inhabited γ
f : (a : α) × (β a → γ) → γ
⊢ f = fun x => f ⟨x.fst, fintypeArrowEquivFinArrow.symm fun i => x.snd (fintypeEquivFin.symm i)⟩