diff --git a/theories/base.v b/theories/base.v
index 2ff07170401f598da3763444a96337be3d299a53..3a72ad1209b1893bef711ebba4904a061e363e54 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -744,6 +744,8 @@ Class FreshSpec A C `{ElemOf A C,
 (** * Booleans *)
 (** The following coercion allows us to use Booleans as propositions. *)
 Coercion Is_true : bool >-> Sortclass.
+Hint Unfold Is_true.
+Hint Resolve orb_prop_intro andb_prop_intro.
 Notation "(&&)" := andb (only parsing).
 Notation "(||)" := orb (only parsing).
 Infix "&&*" := (zip_with (&&)) (at level 40).