Theorem: LO.FirstOrder.UTerm.subtEquiv_fvar (Logic/FirstOrder/Computability/Term.lean)

State before:
L : Language
μ : Type v
n : ℕ
x : μ
⊢ (fvar x).bv ≤ n
Tactic:
simp
State after:
no goals