{ rcases hl with rfl
  simp[encode_nrel, encode_finArrow, List.ofFn_get] }
case pos
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
this :
  Primrec₂ fun r l =>
    if l.length = r.fst then Nat.pair 1 ((Nat.pair 0 ((2 * r.fst.pair) ((encode r.snd).pair (encode l)))).pair 0) + 1
    else 0
k : ℕ
r : L.Rel k
l : List (UTerm L μ)
hl : l.length = k
⊢ Nat.pair 1 ((Nat.pair 0 (2 * k.pair ((encode r).pair (encode l)))).pair 0) =
    encode (nrel r fun i => l.get (Fin.cast ⋯ i))
no goals