RecordConstructorsInErrorMessages.agda:32,7-11
R.A r₁ != A of type Set
when checking that the expression refl has type r₁ ≡ r₂