cases p <;> simp[inversion, bindq, bindqG]
case 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 μ₂
k : σ → ℕ
p✝ : σ → UFormula L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hk : Primrec k
hp : Primrec p✝
hm : Primrec fun q => q.2.2.depth
hl : Primrec LO.FirstOrder.UFormula.bindqL
hg : Primrec₂ (LO.FirstOrder.UFormula.bindqG b e)
x : σ
m : ℕ
p : UFormula L μ₁
⊢ LO.FirstOrder.UFormula.bindqG b e (x, m, p)
      (List.map (fun q => bindq (b q.1) (e q.1) q.2.1 q.2.2)
        (Sum.rec (fun val => [])
          (fun val =>
            Sum.rec (fun val => [])
              (fun val =>
                Sum.rec (fun val => List.map (fun x_1 => (x, m, x_1)) p.inversion.2)
                  (fun val => List.map (fun x_1 => (x, m + 1, x_1)) p.inversion.2) val)
              val)
          p.inversion.1.2)) =
    some (bindq (b x) (e x) m p)
no goals