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

Question

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.

Answer 1

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
*)