cases xs <;> simp_all
case some
α : Type u_1
hd : α
tl xs : List α
x : α
val✝ : List α × α
ho : tl.getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, val✝ = (xs, x) ↔ tl = xs ++ [x]
⊢ hd :: val✝.1 = xs ∧ val✝.2 = x ↔ hd :: tl = xs ++ [x]
case some.nil
α : Type u_1
hd : α
tl : List α
x : α
val✝ : List α × α
ho : tl.getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, val✝ = (xs, x) ↔ tl = xs ++ [x]
⊢ hd = x → ¬tl = []

case some.cons
α : Type u_1
hd : α
tl : List α
x : α
val✝ : List α × α
ho : tl.getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, val✝ = (xs, x) ↔ tl = xs ++ [x]
head✝ : α
tail✝ : List α
⊢ (hd = head✝ ∧ val✝.1 = tail✝) ∧ val✝.2 = x ↔ hd = head✝ ∧ tl = tail✝ ++ [x]