Lemma isfinite_singleton {X : hSet} {x : X} : isfinite (singleton x). Proof. apply isfinitecontr. apply iscontr_singleton. Qed.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions. Require Import UniMath.MoreFoundations.Subtypes.