proposition: Lemma Finite_not_Infinite (A:Type): forall l:LList A, Finite l -> ~ Infinite l.
proof: Proof. simple induction 1. - unfold not in |- *; intro H0; inversion_clear H0. - unfold not at 2 ; intros a l0 H1 H2 H3; inversion H3; auto. Qed.
imports: Arith List RelationClasses