proposition: Lemma Inf_Inf1 {A : Type} : forall l:LList A, Infinite l -> Infinite1 l.
proof: Proof. intros l ; exists (Infinite (A:=A)). split; try assumption. unfold Infinite_ok in |- *. simple destruct l0. - inversion 1. - inversion_clear 1. exists a; exists l1; auto. Qed.