The +-comm in EqualityProofs must have arguments n m 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
+-comminEqualityProofsmust have argumentsnmimplicit (because that's the standard pattern actually used inarend-liband 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).