JasonReedPruning.agda:21,19-23
Refuse to construct infinite term by instantiating _22 to f _22
when checking that the expression refl has type _22 ≡ f _22