Skip to content
GitLab

lemmas to merge a sepL and a sepL2

Merged Ralf Jung requested to merge ralf/big_sepL2_sep into master

These lemmas allow merging a sepL "into" a separate sepL2 if it iterates over one of the 2 lists of the sepL2. Also added some helper lemmas to relate "sepL2 where one list is ignored" with sepL.