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

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