Theorem: SetTheory.interpret_snoc_termSucc (SetTheory/Formula.lean)

State before:
V : Type u_2
inst✝ : SetTheory V
α✝ : Type u_1
v : α✝ → V
n✝ : Nat
l : Fin n✝ → V
y : V
x : α✝ ⊕ Fin n✝
⊢ interpretTerm V v (Fin.snoc l y) (termSucc x) = interpretTerm V v l x
Tactic:
aesop
State after:
no goals