proposition: Lemma True_finite: FiniteT True.
proof: Proof. apply bij_finite with (option False) (fun _ => I). { constructor; constructor. } exists (True_rect None). - destruct x as [[]|]. remember (True_rect (@None False) I) as LHS. destruct LHS as [[]|]. reflexivity. - exact (fun y:True => match y with | I => refl_equal I end). Qed.
imports: Coq(Arith Description FunctionalExtensionality Lia) ZornsLemma(DecidableDec Finite_sets FunctionProperties Image IndexedFamilies Powerset_facts) Coq(ProofIrrelevance)