rintro ⟨⟨⟨x, m, p⟩, l⟩, ⟨k, r, v⟩⟩
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 μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
this : Primrec fun a => (encode a).unpair.2.unpair.2.unpair.2
⊢ ∀ (n : ((σ × ℕ × UFormula L μ₁) × List (UFormula L μ₂)) × (k : ℕ) × L.Rel k × (Fin k → UTerm L μ₁)),
    (encode n).unpair.2.unpair.2.unpair.2 = encode n.2.snd.2
case mk.mk.mk.mk.mk.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 μ
σ : Type u_1
μ₁ : Type u_2
μ₂ : Type u_3
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
this : Primrec fun a => (encode a).unpair.2.unpair.2.unpair.2
l : List (UFormula L μ₂)
x : σ
m : ℕ
p : UFormula L μ₁
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ₁
⊢ (encode (((x, m, p), l), ⟨k, (r, v)⟩)).unpair.2.unpair.2.unpair.2 = encode (((x, m, p), l), ⟨k, (r, v)⟩).2.snd.2