pub fn standardization_theorem_ty() -> Expr
StandardizationTheorem: if t has a normal form, normal order reaches it