Add instance for `FromSep (tc_opaque P) Q1 Q2`

See discussion at !833 (diffs, comment 83516)

• Turns out the cost/comment for FromAnd is obsolete, FromAnd is never used by iCombine
• I removed the Hint Mode for FromAnd that corresponds to it being used by iCombine
• Turns out there was an instance for missing for tc_opaque + FromSep
• I added that instance with the correct cost + a better comment + a test case that used to fail prior to this MR

assigned to @robbertkrebbers

mentioned in merge request !833 (merged)

added 20 commits

• df473eee...55e78d6f - 17 commits from branch master
• 4179bb8a - `FromAnd` is never used for `iCombine`, so remove that mode.
• f8667d35 - Add instance for `FromSep (tc_opaque P) Q1 Q2` and update comment.
• f7255e63 - Add test.

Compare with previous version

Rebased.

The new test makes sense to me. I cannot tell if what you say about iCombine not using FromAnd is correct nor can I fact-check the new comment you added, but it sounds plausible. :D

merged

mentioned in commit 7827fc3f