exact nat_strong_rec'2 _ this (by simp[elimDecodeG_eq_elimDecode β])
α : 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
γ : Type u_4
inst✝¹ : Primcodable σ
inst✝ : Primcodable γ
f : σ → α × List γ → γ
hf : Primrec₂ f
this : Primrec₂ fun p ih => some (WType.SubWType.elimDecodeG β (fun x a ih => f x (a, ih)) p.1 p.2 ih)
⊢ Primrec₂ fun x p => elimDecode β (fun a ih => f x (a, ih)) p.1 p.2
no goals