apply ih
case some.nil
α : Type u_1
hd : α
val✝ : List α × α
ho : [].getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, ¬val✝ = (xs, x)
⊢ False
case some.nil.a
α : Type u_1
hd : α
val✝ : List α × α
ho : [].getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, ¬val✝ = (xs, x)
⊢ val✝ = (?some.nil.xs, ?some.nil.x)

case some.nil.xs
α : Type u_1
hd : α
val✝ : List α × α
ho : [].getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, ¬val✝ = (xs, x)
⊢ List α

case some.nil.x
α : Type u_1
hd : α
val✝ : List α × α
ho : [].getSnoc? = some val✝
ih : ∀ {xs : List α} {x : α}, ¬val✝ = (xs, x)
⊢ α