proposition: Lemma Not_Finite_Infinite : forall (A:Set)(l:LList A), ~ Finite l -> Infinite l.
proof: Proof. cofix H. destruct l. intro; absurd (Finite (LNil (A:=A)));[auto|constructor]. constructor. apply H. red; intro H1;case H0. constructor. trivial. Qed.
imports: Arith Vector List Extraction ZArith Compare_dec ZArith List Wf_nat Bool