pub fn iris_always_ty() -> Expr
IrisAlways: the always modality □P (persistent propositions). Type: IrisProp → IrisProp