induction c <;> simp_all [getSnoc?]
α : Type u_1
c : List α
⊢ c.getSnoc? = none ↔ c = []
case cons
α : Type u_1
head✝ : α
tail✝ : List α
tail_ih✝ : tail✝.getSnoc? = none ↔ tail✝ = []
⊢ ¬(match tail✝.getSnoc? with
      | none => some ([], head✝)
      | some (xs', x') => some (head✝ :: xs', x')) =
      none