[catnaroek]

The type constructor that's being assumed injective in the section “Deriving `absurd` with type families” is `R`.