apply this
τ : 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)) = 2
hf : Primrec f
this✝ : Primrec₂ fun x w => (encode (mkL (f x) [w.1, w.2])).pred
x : σ
x✝ : WType β × WType β
w₁ w₂ : WType β
this : Function.Injective ⇑(fintypeArrowEquivFinArrow' ⋯)
⊢ (fintypeArrowEquivFinArrow.symm fun i => [w₁, w₂].get (Fin.cast ⋯ i)) = (fintypeArrowEquivFinArrow' ⋯).symm ![w₁, w₂]
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)) = 2
hf : Primrec f
this✝ : Primrec₂ fun x w => (encode (mkL (f x) [w.1, w.2])).pred
x : σ
x✝ : WType β × WType β
w₁ w₂ : WType β
this : Function.Injective ⇑(fintypeArrowEquivFinArrow' ⋯)
⊢ (fintypeArrowEquivFinArrow' ⋯) (fintypeArrowEquivFinArrow.symm fun i => [w₁, w₂].get (Fin.cast ⋯ i)) =
    (fintypeArrowEquivFinArrow' ⋯) ((fintypeArrowEquivFinArrow' ⋯).symm ![w₁, w₂])