Issue644.agda:28,13-14 R !=< ((x : A) → P x) of type Set₁ when checking that the expression r has type (x : A) → P x