aboutsummaryrefslogtreecommitdiff
path: root/src/Util
diff options
context:
space:
mode:
Diffstat (limited to 'src/Util')
-rw-r--r--src/Util/ListUtil.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index 88fb815b2..4d6555778 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -1101,7 +1101,7 @@ Proof.
intuition (subst; auto).
Qed.
-Lemma fold_right_invariant : forall {A} P (f: A -> A -> A) l x,
+Lemma fold_right_invariant : forall {A B} P (f: A -> B -> B) l x,
P x -> (forall y, In y l -> forall z, P z -> P (f y z)) ->
P (fold_right f x l).
Proof.