Definition ischoicebasefiniteset {X : UU} (xf : isfinite X) : ischoicebase X. Proof. use(hinhuniv _ xf). intros [n w]. exact(ischoicebaseweqf w (ischoicebasestn n)). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions. Require Import UniMath.MoreFoundations.Subtypes.