diff --git a/theories/base.v b/theories/base.v
index 1d35448e8c2d753375a6e5891afe7f009a2b0178..b7b02e23078068d7a642ad2b1254317f1358c6d9 100644
--- a/theories/base.v
+++ b/theories/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/theories/decidable.v b/theories/decidable.v
index 545cafe2deac2dbca5fd08b7ba7fe3af64313ffc..8f45a83e25d5a8b9fdf4bdbac69f427f85d4c87e 100644
--- a/theories/decidable.v
+++ b/theories/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).