Another definition of infinite lists

Consider the following definitions :
Definition Infinite_ok (A:Set) (X:LList A -> Prop) :=
  forall l:LList A,
    X l ->  exists a : A | ( exists l' : LList A | l = LCons a l' /\ X l').
Definition Infinite1 (A:Set) (l:LList A) :=
   exists X : LList A -> Prop | Infinite_ok X /\ X l.

Prove that the predicates Infinite1 and Infinite are logically equivalent.
A context for starting your work
The solution

Going home
Pierre Castéran