apply Option.some.inj
α : Type u
β : Type v
γ : Type w
l : List α
a : α
h : length l < length (l ++ [a])
⊢ get (l ++ [a]) { val := length l, isLt := h } = a
case x
α : Type u
β : Type v
γ : Type w
l : List α
a : α
h : length l < length (l ++ [a])
⊢ some (get (l ++ [a]) { val := length l, isLt := h }) = some a