Theorem: LO.FirstOrder.Semiterm.bv_subtEquiv (Logic/FirstOrder/Computability/Term.lean)

State before:
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n : ℕ
t : Semiterm L μ n
⊢ (↑(subtEquiv t)).bv ≤ n
Tactic:
induction t <;> simp [UTerm.bv]
State after:
case bvar
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n : ℕ
a✝ : Fin n
⊢ ↑a✝ + 1 ≤ n

State before:
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n : ℕ
x : Fin n
⊢ ↑x + 1 ≤ n
Tactic:
case bvar x => exact x.prop
State after:
no goals

State before:
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n : ℕ
x : Fin n
⊢ ↑x + 1 ≤ n
Tactic:
exact x.prop
State after:
no goals