Theorem: LO.FirstOrder.UFormula.subfEquiv_and (Logic/FirstOrder/Computability/Formula.lean)

State before:
L : Language
μ : Type v
n : ℕ
p q : Semiformula L μ n
⊢ ((↑(subfEquiv p)).and ↑(subfEquiv q)).bv ≤ n
Tactic:
simp
State after:
no goals