proposition: Lemma Inf1_Inf {A : Type}: forall l:LList A, Infinite1 l -> Infinite l.
proof: Proof. cofix Inf1_Inf. simple destruct l. - intro H; case (Infinite1_LNil H). - intros a l0 H0; generalize (Infinite1_LCons H0); constructor. now apply Inf1_Inf. Qed.