A Universe of Sorts

$R_\tau(e)$ has three conditions:
(1) $e$ has type $\tau$
(2) $e$ has the property of interest ( $e$ strongly normalizes / has normal form)
(3) The set $R\tau$ is closed under eliminators!
My intuition for (3) is that expressions are "freely built" under constructors. On the other hand, it is eliminators that perform computation, so we need $R_\tau$ to be closed under "computation" or "elimination"
Video

§ Logical Predicates (OPLSS '12)