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