proposition: Lemma FiniteT_unit : FiniteT unit.
proof: Proof. unshelve eapply bij_finite with (X := option False). - intros. constructor. - repeat constructor. - unshelve econstructor. + intros. exact None. + intros. destruct x; intuition. + intros. destruct y; intuition. Qed.
imports: Coq(Arith Description FunctionalExtensionality Lia) ZornsLemma(DecidableDec Finite_sets FunctionProperties Image IndexedFamilies Powerset_facts) Coq(ProofIrrelevance)