rcases this with ⟨hi, rfl⟩
case pos.right.a.a.some
τ : 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)
i c : ℕ
w : WType β
hw : l.get? i = some w
this : ∃ (hi : i < l.length), l.get ⟨i, hi⟩ = w
⊢ (encode w).unpair.2 = c ↔ ∃ (h_1 : i < Fintype.card (β a)), (encode (l.get ⟨i, ⋯⟩)).unpair.2 = c
case pos.right.a.a.some.intro
τ : 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)
i c : ℕ
hi : i < l.length
hw : l.get? i = some (l.get ⟨i, hi⟩)
⊢ (encode (l.get ⟨i, hi⟩)).unpair.2 = c ↔ ∃ (h_1 : i < Fintype.card (β a)), (encode (l.get ⟨i, ⋯⟩)).unpair.2 = c