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

State before:
L : Language
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
m : ℕ
e : μ₁ → UTerm L μ₂
t : UTerm L μ₁
ht : t.bv ≤ m
he : ∀ (x : μ₁), (e x).bv ≤ m
x : ℕ
hx : x < t.bv
⊢ (bvar x).bv ≤ m
Tactic:
simp
State after:
L : Language
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
m : ℕ
e : μ₁ → UTerm L μ₂
t : UTerm L μ₁
ht : t.bv ≤ m
he : ∀ (x : μ₁), (e x).bv ≤ m
x : ℕ
hx : x < t.bv
⊢ x + 1 ≤ m

State before:
L : Language
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
m : ℕ
e : μ₁ → UTerm L μ₂
t : UTerm L μ₁
ht : t.bv ≤ m
he : ∀ (x : μ₁), (e x).bv ≤ m
x : ℕ
hx : x < t.bv
⊢ x + 1 ≤ m
Tactic:
exact lt_of_lt_of_le hx ht
State after:
no goals