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

State before:
L : Language
μ : Type v
n k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n
⊢ (nrel r fun i => ↑(UTerm.subtEquiv (v i))).bv ≤ n
Tactic:
simp
State after:
no goals