Strenghten In_size lemma

MetaCoq · Jan 24, 2024 · c5cb1ab · c5cb1ab
1 parent 4dc7c47
commit c5cb1ab
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/utils/theories/MCList.v b/utils/theories/MCList.v
@@ -1406,7 +1406,7 @@ Proof.
 Qed.
 
 Lemma In_size {A B} {x : A} {l : list A} (proj : A -> B) (size : B -> nat) :
-  In x l -> size (proj x) < S (list_size (size ∘ proj) l).
+  In x l -> size (proj x) < (list_size (size ∘ proj) l).
 Proof.
   induction l; cbn => //.
   intros [->|hin]. lia. specialize (IHl hin); lia.