generalize ho : getSnoc? tl = o at ih
α : Type u_1
hd : α
tl : List α
ih : ∀ {xs : List α} {x : α}, tl.getSnoc? = some (xs, x) ↔ tl = xs ++ [x]
xs : List α
x : α
⊢ (match tl.getSnoc? with
      | none => some ([], hd)
      | some (xs', x') => some (hd :: xs', x')) =
      some (xs, x) ↔
    hd :: tl = xs ++ [x]
α : Type u_1
hd : α
tl xs : List α
x : α
o : Option (List α × α)
ho : tl.getSnoc? = o
ih : ∀ {xs : List α} {x : α}, o = some (xs, x) ↔ tl = xs ++ [x]
⊢ (match o with
      | none => some ([], hd)
      | some (xs', x') => some (hd :: xs', x')) =
      some (xs, x) ↔
    hd :: tl = xs ++ [x]