Definition isfinite_to_DecidableEquality {X : UU} : isfinite X -> DecidableRelation X. Proof. intros fin x y. exact (@isdecprop_to_DecidableProposition (x=y) (isdecpropif (x=y) (isfinite_isaset X fin x y) (isfinite_isdeceq X fin x y))). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions. Require Import UniMath.MoreFoundations.Subtypes.