diff --git a/prelude/base.v b/prelude/base.v
index 1d35448e8c2d753375a6e5891afe7f009a2b0178..b7b02e23078068d7a642ad2b1254317f1358c6d9 100644
--- a/prelude/base.v
+++ b/prelude/base.v
@@ -374,6 +374,8 @@ Notation zip := (zip_with pair).
 Coercion Is_true : bool >-> Sortclass.
 Hint Unfold Is_true.
 Hint Immediate Is_true_eq_left.
+Existing Class Is_true.
+Instance true_Is_true : Is_true true := I.
 Hint Resolve orb_prop_intro andb_prop_intro.
 Notation "(&&)" := andb (only parsing).
 Notation "(||)" := orb (only parsing).
diff --git a/prelude/decidable.v b/prelude/decidable.v
index 76ec221035db68e9da9146cf98d9dd18056e4fc6..7b6431a6f371b738060c9d957440c276e4c44270 100644
--- a/prelude/decidable.v
+++ b/prelude/decidable.v
@@ -146,7 +146,7 @@ Proof. apply dsig_eq; reflexivity. Qed.
 Instance True_dec: Decision True := left I.
 Instance False_dec: Decision False := right (False_rect False).
 Instance Is_true_dec b : Decision (Is_true b).
-Proof. destruct b; apply _. Defined.
+Proof. destruct b; simpl; apply _. Defined.
 
 Section prop_dec.
   Context `(P_dec : Decision P) `(Q_dec : Decision Q).