proposition: Lemma Infinite1_LCons {A: Type} : forall (a:A) (l:LList A), Infinite1 (LCons a l) -> Infinite1 l.
proof: Proof. intros a l H. case H; intros X HX; case HX; intros H1 H2; clear HX. exists (fun u:LList A => exists b : A, X (LCons b u)); split. - unfold Infinite_ok in |- *. intros l0 [b Hb]. assert (H4 : X l0) by apply (ok_LCons _ _ H1 Hb);eauto. case (H1 l0 H4); intros x [l' [el' Hl']]. exists x, l'; split; try assumption. exists x; rewrite <- el'; auto. - exists a; auto. Qed.