Arguments of +-comm should be implicit

[sxhya]

trafficstars

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).