Inconsistent order of arguments for `inv_alloc` and `cinv_alloc`.
inv_alloc: ∀ (N : namespace) (E : coPset) (P : iProp Σ), ▷ P ={E}=∗ inv N P
vs
cinv_alloc: ∀ (E : coPset) (N : namespace) (P : iPropSI Σ),
▷ P ={E}=∗ ∃ γ : gname, cinv N γ P ∗ cinv_own γ 1
As you can see, inv_alloc
first takes the namespace and then the mask, but cinv_alloc
first takes the mask and the the namespace.