proposition: Lemma FiniteT_bool : FiniteT bool.
proof: Proof. unshelve eapply bij_finite with (X := option (option False)). - intros. refine (match H with | None => true | Some _ => false end). - repeat constructor. - unshelve econstructor. + intros. apply (match H with | true => None | false => Some None end). + intros. destruct x as [[]|]; intuition. + intros. destruct y as [|]; intuition. Qed.
imports: Coq(Arith Description FunctionalExtensionality Lia) ZornsLemma(DecidableDec Finite_sets FunctionProperties Image IndexedFamilies Powerset_facts) Coq(ProofIrrelevance)