Theorem: LO.FirstOrder.Semiterm.Operator.val_bvar (Logic/FirstOrder/Basic/Operator.lean)

State before:
L : Language
M : Type w
s : Structure L M
n : ℕ
x : Fin n
v : Fin n → M
⊢ (bvar x).val v = v x
Tactic:
simp [Operator.bvar, Operator.val]
State after:
no goals