pub fn iris_auth_ty() -> Expr
IrisAuth: authoritative element in the auth camera. Type: {A : Type} → A → IrisProp