Use more appropriate lemma

17 jobs for shorten-proof in 9 minutes and 58 seconds (queued for 5 seconds)
Status Job ID Name Coverage
  Build
passed #77940
1.10.0-coq-8.10

00:09:34

passed #77941
1.10.0-coq-8.11

00:09:38

passed #77939
1.10.0-coq-8.9

00:09:29

passed #77937
1.9.0-coq-8.10

00:09:24

passed #77938
1.9.0-coq-8.11

00:05:26

passed #77936
1.9.0-coq-8.9

00:05:21

passed #77942
build-for-process

00:03:36

passed #77943
build-for-process-classic

00:06:35

failed #77946
allowed to fail
coq-8.10

00:04:44

failed #77947
allowed to fail
coq-dev

00:03:16

passed #77944
proof-length

00:00:49

passed #77945
spell-check

00:01:06

 
  Process
passed #77950
doc

00:00:43

passed #77951
doc-classic

00:01:04

passed #77952
proof-state

00:06:16

passed #77948
validate

00:01:05

passed #77949
validate-classic

00:02:11

 
Name Stage Failure
failed
coq-8.10 Build


<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-prosa dev
+-
- No changes have been performed
'opam install -y -v -j 2 coq-prosa' failed.
ERROR: Job failed: exit code 1
failed
coq-dev Build
# make[1]: *** Waiting for unfinished jobs....
# make: *** [Makefile:343: all] Error 2

+- The following actions failed
| - build coq-prosa dev
+-
- No changes have been performed
'opam install -y -v -j 2 coq-prosa' failed.
ERROR: Job failed: exit code 1