proposition: Lemma Not_Infinite_Finite {A:Type}: forall l:LList A, ~ Infinite l -> Finite l.
proof: Proof. intros l H; case (classic (Finite l)). - trivial. - intro H0; destruct H; now apply Not_Finite_Infinite. Qed.
imports: chap13 Classical