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)
⊢ ∀ (a : σ) (n m : ℕ),
    some
        (WType.SubWType.elimDecodeG β (fun x a ih => f x (a, ih)) (a, n, m).1 (a, n, m).2
          (List.map (fun i => elimDecode β (fun a_1 ih => f a (a_1, ih)) i.unpair.1 i.unpair.2)
            (List.range (n.pair m)))) =
      some (elimDecode β (fun a_1 ih => f a (a_1, ih)) (n, m).1 (n, m).2)
no goals