Agda-2.3.2.2: test/fail/TerminationOnIrrelevant.err
TerminationOnIrrelevant.agda:24,15-19 f x != g y of type ⊥ when checking that the expression refl has type f x ≡ g y
TerminationOnIrrelevant.agda:24,15-19 f x != g y of type ⊥ when checking that the expression refl has type f x ≡ g y