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: Ensembles EnsemblesImplicit Image ImageImplicit Finite_sets FunctionProperties DecidableDec ProofIrrelevance Description