The +-comm in EqualityProofs must have arguments nm implicit (because that's the standard pattern actually used in arend-lib and everywhere else in the tutorial). Maybe you need to explain somewhere how the signature of a definition should be chosen (which arguments should be made implicit and which explicit).
The
+-comm
inEqualityProofs
must have argumentsn
m
implicit (because that's the standard pattern actually used inarend-lib
and everywhere else in the tutorial). Maybe you need to explain somewhere how the signature of a definition should be chosen (which arguments should be made implicit and which explicit).