Require Import Coinduc. Require Import Classical. Lemma Not_Infinite_Finite : forall (A:Set) (l:LList A), ~ Infinite l -> Finite l. Lemma Finite_or_Infinite : forall (A:Set)(l:LList A), Finite l \/ Infinite l.