pub fn invariant_alloc_ty() -> Expr
InvariantAlloc: allocate a new invariant. Type: {P : IrisProp} → P ⊢ |==> ∃ N, inv(N, P)