Theorem: LO.FirstOrder.UFormula.bindq_param_primrec
Proof state before:
case 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 μ₂
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 μ₁
x₂ : σ
m₂ : ℕ
p₂ : UFormula L μ₁
⊢ (x₂, m₂, p₂) ∈
      Sum.rec (fun val => [])
        (fun val =>
          Sum.rec (fun val => [])
            (fun val =>
              Sum.rec (fun val => List.map (fun x => (x₁, m₁, x)) p₁.inversion.2)
                (fun val => List.map (fun x => (x₁, m₁ + 1, x)) p₁.inversion.2) val)
            val)
        p₁.inversion.1.2 →
    p₂.depth < p₁.depth
Tactic:
cases p₁ <;> simp[inversion]
Proof state after:
case mk.mk.mk.mk.and
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₁ : ℕ
x₂ : σ
m₂ : ℕ
p₂ a✝¹ a✝ : UFormula L μ₁
⊢ x₂ = x₁ ∧ m₂ = m₁ ∧ p₂ = a✝¹ ∨ x₂ = x₁ ∧ m₂ = m₁ ∧ p₂ = a✝ → p₂.depth < (a✝¹.and a✝).depth

case mk.mk.mk.mk.or
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₁ : ℕ
x₂ : σ
m₂ : ℕ
p₂ a✝¹ a✝ : UFormula L μ₁
⊢ x₂ = x₁ ∧ m₂ = m₁ ∧ p₂ = a✝¹ ∨ x₂ = x₁ ∧ m₂ = m₁ ∧ p₂ = a✝ → p₂.depth < (a✝¹.or a✝).depth

case mk.mk.mk.mk.all
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₁ : ℕ
x₂ : σ
m₂ : ℕ
p₂ a✝ : UFormula L μ₁
⊢ x₂ = x₁ → m₂ = m₁ + 1 → p₂ = a✝ → p₂.depth < a✝.all.depth

case mk.mk.mk.mk.ex
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₁ : ℕ
x₂ : σ
m₂ : ℕ
p₂ a✝ : UFormula L μ₁
⊢ x₂ = x₁ → m₂ = m₁ + 1 → p₂ = a✝ → p₂.depth < a✝.ex.depth