Goal:
    A : Type  P : list A → Type
  ============================
   (P [] → (∀ (l : list A) (x : A), P (l ++ [x])) → ∀ l : list A, P l)


DEBUG:Going to execute:
intros
DEBUG LTAC Evaluated term: skipn_all_app