Separation_Logic_Unbounded.WandProperties