Theorem: Fin.snoc_apply (SetTheory/Formula.lean)

State before:
V : Type ?u.8297
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x : α
⊢ snoc l x { val := n, isLt := (_ : n < Nat.succ n) } = x
Tactic:
simp only [snoc]
State after:
V : Type ?u.8297
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x : α
⊢ (if h : n < n then l { val := n, isLt := (_ : { val := n, isLt := (_ : n < Nat.succ n) }.val < n) } else x) = x

State before:
V : Type ?u.8297
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x : α
⊢ (if h : n < n then l { val := n, isLt := (_ : { val := n, isLt := (_ : n < Nat.succ n) }.val < n) } else x) = x
Tactic:
aesop
State after:
no goals