Michael Sammler
--- a/theories/base.v
+++ b/theories/base.v
 Existing Class TCTrue.
 Existing Instance TCTrue_intro.

+Inductive TCFalse : Prop :=.
+Existing Class TCFalse.
+
+Notation TCUnless P := (TCIf P TCFalse TCTrue).
--- a/theories/base.v
+++ b/theories/base.v
 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).
--- a/theories/list.v
+++ b/theories/list.v
 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.