Make `big_op{L,M}_gen_proper_2` stronger

The existing versions did not allow the two structures to be over different types.

Solves #262

This sounds like a good generalization, thanks! I noticed that I used the generalization already for big_sepL2_proper_2 and big_sepM2_proper_2, but forgot it here.

added 1 commit

• 481c49d6 - Make `big_op{L,M}_gen_proper_2` stronger

Compare with previous version

added 14 commits

• 481c49d6...e2f65bbd - 12 commits from branch iris:master
• 8a4fd004 - Move some lemmas about big_opM outside the section
• 39f0153e - Make types of `big_op{L,M}_gen_proper_2` more generic

Compare with previous version

resolved all threads

resolved all threads

merged

mentioned in commit 4f90bb04

Thanks & merged.