Agda-2.3.2.2: test/fail/NotApplyingInDontCareTriggersInternalError.err
NotApplyingInDontCareTriggersInternalError.agda:49,60-73 Variable leftRefl is declared irrelevant, so it cannot be used here when inferring the type of leftRefl a≼a'
NotApplyingInDontCareTriggersInternalError.agda:49,60-73 Variable leftRefl is declared irrelevant, so it cannot be used here when inferring the type of leftRefl a≼a'