rintro ⟨k, r⟩ l
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 1 ((2 * r.fst.pair) ((encode r.snd).pair (encode l)))).pair 0) + 1
    else 0
⊢ ∀ (a : (k : ℕ) × L.Rel k) (b : List (UTerm L μ)),
    (if b.length = a.fst then Nat.pair 1 ((Nat.pair 1 ((2 * a.fst.pair) ((encode a.snd).pair (encode b)))).pair 0) + 1
      else 0) =
      encode (relL a b)
case mk
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 1 ((2 * r.fst.pair) ((encode r.snd).pair (encode l)))).pair 0) + 1
    else 0
k : ℕ
r : L.Rel k
l : List (UTerm L μ)
⊢ (if l.length = ⟨k, r⟩.fst then
      Nat.pair 1 ((Nat.pair 1 ((2 * ⟨k, r⟩.fst.pair) ((encode ⟨k, r⟩.snd).pair (encode l)))).pair 0) + 1
    else 0) =
    encode (relL ⟨k, r⟩ l)