proposition: Lemma nat_infinite: ~ FiniteT nat.
proof: Proof. red; intro. assert (surjective S). apply finite_inj_surj; trivial. red; intros. injection H0; trivial. destruct (H0 0). discriminate H1. Qed.
imports: FiniteTypes EnsemblesImplicit ClassicalChoice Arith FunctionalExtensionality EnsemblesSpec