proposition: Lemma Not_Finite_Infinite (A:Type): forall l:LList A, ~ Finite l -> Infinite l.
proof: Proof. cofix H. simple destruct l. - intros; absurd (Finite (LNil (A:=A))); auto with llists. - split; apply H; unfold not in |- *; intro H1. apply H0; auto with llists. Qed.
imports: Arith List RelationClasses