Theorem: LO.FirstOrder.Semiformula.bv_subtEquiv (Logic/FirstOrder/Computability/Formula.lean)

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n : ℕ
p : Semiformula L μ n
⊢ (↑(subfEquiv p)).bv ≤ n
Tactic:
induction p <;> simp
State after:
no goals