simp[encode_fintypeArrow, encode_finArrow]
case pos.right
τ : 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 γ
this :
  Primrec₂ fun a l =>
    if l.length = Fintype.card (β a) then
      ((List.map depth l).sup + 1).pair ((encode a).pair (encode (List.map (fun w => (encode w).unpair.2) l))) + 1
    else 0
a : α
l : List (WType β)
h : l.length = Fintype.card (β a)
⊢ encode (List.map (fun w => (encode w).unpair.2) l) =
    encode fun b => (encode (l.get (Fin.cast ⋯ (fintypeEquivFin b)))).unpair.2
case pos.right
τ : 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 γ
this :
  Primrec₂ fun a l =>
    if l.length = Fintype.card (β a) then
      ((List.map depth l).sup + 1).pair ((encode a).pair (encode (List.map (fun w => (encode w).unpair.2) l))) + 1
    else 0
a : α
l : List (WType β)
h : l.length = Fintype.card (β a)
⊢ List.map (fun w => (encode w).unpair.2) l =
    List.ofFn (fintypeArrowEquivFinArrow fun b => (encode (l.get (Fin.cast ⋯ (fintypeEquivFin b)))).unpair.2)