diff --git a/theories/base.v b/theories/base.v
index 309a844f0895c301fd33c1e4e390fd59c9ffbb7e..af97a3f70a0af2bee5f0cfb72525ac8e58b51b72 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -127,6 +127,19 @@ Inductive TCTrue : Prop := TCTrue_intro : TCTrue.
 Existing Class TCTrue.
 Existing Instance TCTrue_intro.
 
+(** The class [TCFalse] is not stricly necessary as one could also use
+[False]. However, users might expect that TCFalse exists and if it
+does not, it can cause hard to diagnose bugs due to automatic
+generalization. *)
+Inductive TCFalse : Prop :=.
+Existing Class TCFalse.
+
+(** The class [TCUnless] can be used to check that search for [P]
+fails. This is useful as a guard for certain instances together with
+classes like [TCFastDone] (see [tactics.v]) to prevent infinite loops
+(e.g. when saturating the context). *)
+Notation TCUnless P := (TCIf P TCFalse TCTrue).
+
 Inductive TCForall {A} (P : A → Prop) : list A → Prop :=
   | TCForall_nil : TCForall P []
   | TCForall_cons x xs : P x → TCForall P xs → TCForall P (x :: xs).
@@ -148,6 +161,14 @@ Existing Instance TCForall2_cons.
 Global Hint Mode TCForall2 ! ! ! ! - : typeclass_instances.
 Global Hint Mode TCForall2 ! ! ! - ! : typeclass_instances.
 
+Inductive TCExists {A} (P : A → Prop) : list A → Prop :=
+  | TCExists_cons_hd x l : P x → TCExists P (x :: l)
+  | TCExists_cons_tl x l: TCExists P l → TCExists P (x :: l).
+Existing Class TCExists.
+Existing Instance TCExists_cons_hd | 10.
+Existing Instance TCExists_cons_tl | 20.
+Global Hint Mode TCExists ! ! ! : typeclass_instances.
+
 Inductive TCElemOf {A} (x : A) : list A → Prop :=
   | TCElemOf_here xs : TCElemOf x (x :: xs)
   | TCElemOf_further y xs : TCElemOf x xs → TCElemOf x (y :: xs).
diff --git a/theories/list.v b/theories/list.v
index 68ca3f6eb5501bf3db7a4bd41b151ba9802c0502..8c80c6a1b27294af2eb4c9f5a0ae65da9f9d5e66 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -4320,6 +4320,9 @@ Proof. rewrite !TCForall_Forall. apply Forall_app_2. Qed.
 Lemma TCForall2_Forall2 {A B} (P : A → B → Prop) xs ys : TCForall2 P xs ys ↔ Forall2 P xs ys.
 Proof. split; induction 1; constructor; auto. Qed.
 
+Lemma TCExists_Exists {A} (P : A → Prop) l : TCExists P l ↔ Exists P l.
+Proof. split; induction 1; constructor; solve [auto]. Qed.
+
 Section positives_flatten_unflatten.
   Local Open Scope positive_scope.
 
diff --git a/theories/tactics.v b/theories/tactics.v
index fa215d8707422c2ac1110362866bec6cb181092f..f7bd6468da050c2ecd803a24a408c2b70675177b 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -44,6 +44,9 @@ Ltac fast_done :=
 Tactic Notation "fast_by" tactic(tac) :=
   tac; fast_done.
 
+Class TCFastDone (P : Prop) : Prop := tc_fast_done : P.
+Global Hint Extern 1 (TCFastDone ?P) => (change P; fast_done) : typeclass_instances.
+
 (** A slightly modified version of Ssreflect's finishing tactic [done]. It
 also performs [reflexivity] and uses symmetry of negated equalities. Compared
 to Ssreflect's [done], it does not compute the goal's [hnf] so as to avoid