proposition: Lemma isfinite_singleton {X : hSet} {x : X} : isfinite (singleton x).
proof: Proof. apply isfinitecontr. apply iscontr_singleton. Qed.
imports: UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions UniMath.Combinatorics.StandardFiniteSets UniMath.MoreFoundations.Subtypes