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

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

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