Definition kfinite_subtype_property {X} (A : kfinite_subtype X) : iskfinite (carrier A) := pr2 A.
Require Import UniMath.Foundations.Propositions. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.Combinatorics.FiniteSets. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.Combinatorics.KFiniteTypes.