simp[relL]
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 σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
hb : Primrec₂ b
he : Primrec₂ e
l : List (UFormula L μ₂)
x : σ
m : ℕ
p : UFormula L μ₁
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ₁
⊢ relL ⟨(((x, m, p), l), ⟨k, (r, v)⟩).2.fst, (((x, m, p), l), ⟨k, (r, v)⟩).2.snd.1⟩
      (List.map
        (fun t =>
          UTerm.bind (shiftb (b (((x, m, p), l), ⟨k, (r, v)⟩).1.1.1) (((x, m, p), l), ⟨k, (r, v)⟩).1.1.2.1)
            (fun x_1 => UTerm.bShifts (((x, m, p), l), ⟨k, (r, v)⟩).1.1.2.1 (e (((x, m, p), l), ⟨k, (r, v)⟩).1.1.1 x_1))
            t)
        (List.ofFn (((x, m, p), l), ⟨k, (r, v)⟩).2.snd.2)) =
    some
      (rel (((x, m, p), l), ⟨k, (r, v)⟩).2.snd.1 fun i =>
        UTerm.bind (shiftb (b (((x, m, p), l), ⟨k, (r, v)⟩).1.1.1) (((x, m, p), l), ⟨k, (r, v)⟩).1.1.2.1)
          (fun x_1 => UTerm.bShifts (((x, m, p), l), ⟨k, (r, v)⟩).1.1.2.1 (e (((x, m, p), l), ⟨k, (r, v)⟩).1.1.1 x_1))
          ((((x, m, p), l), ⟨k, (r, v)⟩).2.snd.2 i))
no goals