The existing big_sep*_sep lemmas work with rewrite and iApply, but not for forward reasoning with iDestruct.