Integration into normalization by evaluation

data TmStx = ... | If TmStx TmStx TmStx
data TyStx = ... | Bool

data TmVal = ... | VOpaque
data TyVal = ... | VBool

isSmall :: TyVal -> Bool

reflect :: TyVal -> Lvl -> Val
reflect a l
  | isSmall a = VOpaque
  ...

eval :: Env -> TmStx -> TmVal
eval (If _ _ _) = VOpaque
...