How to do induction on the end of a list in Coq

In the standart way I have induction for list like this

• Approval is performed for lst
• Proving for x::lst

But I want:

• Approval is performed for lst
• Proving for lst ++ x::nil

For me, the place of x in the list is important.

I tried to write something like this, but not successful.

In such case, you need to prove your own induction principle. But here you're lucky because what you need is already in the standard library of Coq:

Require Import List.

Check rev_ind.
(*
rev_ind
     : forall (A : Type) (P : list A -> Prop),
       P nil ->
       (forall (x : A) (l : list A), P l -> P (l ++ x :: nil)) ->
       forall l : list A, P l
*)