diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index f699c43ed3..f711b8e397 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -8,6 +8,8 @@
   + lemmas `seriesN`, `seriesD`, `seriesZ`, `is_cvg_seriesN`, `lim_seriesN`,
     `is_cvg_seriesZ`, `lim_seriesZ`, `is_cvg_seriesD`, `lim_seriesD`,
     `is_cvg_seriesB`, `lim_seriesB`, `lim_series_le`, `lim_series_norm`
+- in `boolp.v`:
+  + definitions `equality_mixin_of_Type`, `choice_of_Type`
 
 ### Changed
 
diff --git a/theories/boolp.v b/theories/boolp.v
index 3c059dc4f2..d00fa445c3 100644
--- a/theories/boolp.v
+++ b/theories/boolp.v
@@ -238,6 +238,12 @@ Proof. by case: asboolP. Qed.
 Lemma asboolF (P : Prop) : ~ P -> `[<P>] = false.
 Proof. by apply/introF/asboolP. Qed.
 
+Definition equality_mixin_of_Type (T : Type) : Equality.mixin_of T :=
+  EqMixin (fun x y : T => asboolP (x = y)).
+
+Definition choice_of_Type (T : Type) : choiceType :=
+  Choice.Pack (Choice.Class (equality_mixin_of_Type T) gen_choiceMixin).
+
 Lemma is_true_inj : injective is_true.
 Proof. by move=> [] []; rewrite ?(trueE, falseE) ?propeqE; tauto. Qed.