pub fn stlc_strong_normalization_ty() -> Expr
STLCStrongNormalization: all well-typed STLC terms are strongly normalizing