proposition: Lemma nf_of_finite : forall n b, nf (cons zero n b) -> b = zero.
proof: Proof. intros n b H; inversion_clear H. trivial. case (not_lt_zero (a:=a'));auto. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List