add lemmas for na_own p ∅

This MR adds lemmas and instances for the non-atomic invariant token na_own p E for when E is ∅.