no goals
α : Type u_1
β : Type ?u.667113
inst✝ : DecidableEq α
l : List α
x✝ x : α
xs : List α
⊢ ↑(formPerm (x :: xs)) (getLast (x :: xs) (_ : x :: xs ≠ [])) = x
induction' xs using List.reverseRecOn with xs y _ generalizing x <;> simp