aboutsummaryrefslogtreecommitdiff
path: root/src/Util/ListUtil/FoldBool.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Util/ListUtil/FoldBool.v')
-rw-r--r--src/Util/ListUtil/FoldBool.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Util/ListUtil/FoldBool.v b/src/Util/ListUtil/FoldBool.v
index f6cac6118..528b6ea25 100644
--- a/src/Util/ListUtil/FoldBool.v
+++ b/src/Util/ListUtil/FoldBool.v
@@ -1,5 +1,6 @@
Require Import Coq.Classes.Morphisms.
Require Import Coq.Lists.List.
+Import ListNotations. Open Scope bool_scope.
Lemma fold_left_orb_true ls
: List.fold_left orb ls true = true.