Another definition of infinite lists

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.