Lemma 5.8.2. from the book #3040
Annotations
1 error
|
Run coq-community/docker-coq-action@v1:
contrib/HoTTBook.v#L783
The reference HoTT.PathAny.contr_pfammap_identitysystem was not found
in the current environment.
Command exited with non-zero status 1
|
Loading