Skip to content

add big_sep*_sep_2 lemmas for merging bigops via iDestruct

Ralf Jung requested to merge ralf/big-sep_2 into master

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

Merge request reports