proposition: Lemma Infinite_not_Finite (A:Type) : forall l:LList A, Infinite l -> ~ Finite l.
proof: Proof. unfold not in |- *; intros l H H0. absurd (Infinite l); auto. apply Finite_not_Infinite; auto. Qed.
imports: Arith List RelationClasses