proposition: Lemma Finite_not_Infinite : forall (A:Set)(l:LList A), Finite l -> ~ Infinite l.
proof: Proof. intros A l H; elim H. apply LNil_not_Infinite. intros a l0 F0 I0' I1. case I0'; inversion_clear I1. trivial. Qed.
imports: Arith Vector List Extraction ZArith Compare_dec ZArith List Wf_nat Bool