A recursor for Finite

Proposed by Vincent Filou.
Define the following recursor:

Finite_rect :
forall (A : Type) (P : LList A -> Type),
P (LNil A) ->
(forall (x : A) (l : LList A), P l -> P (LCons x l)) ->
forall l : LList A, Finite l -> P l

Hint
Define an inductive predicate with only one constructor, equivalent to Finite, such that Coq generates an elimination principle for sort Type>.
Use Finite_rect for defining a function that maps any finite Llist to a list:

Fixpoint llist_injection (A:Set) (l:list A) {struct l} : 
 LList A :=
  match l with
  | nil => LNil
  | a :: l' => LCons a (llist_injection l')
  end.

Definition to_list_strong: to_list_strong
     : forall (A : Type) (x : LList A),
       Finite x -> {l : list A | x = list_injection A l}.

Solution

Follow this link
An alternate version contributed by Damien Pous