na_inv: tweak definition
Debatable, but the proof context of `na_inv_alloc` writes `ε` instead of `CoPSet ∅`.
Loading
Please register or sign in to comment
Debatable, but the proof context of `na_inv_alloc` writes `ε` instead of `CoPSet ∅`.