Make `unseal` tactics type-directed

The unseal tactics have to go through two layers:

1. Unfold the projections of the BI canonical structures/classes (e.g., bi_sep)
2. Unfold the definition of the instance

Step (1) is currently implemented using unfold and step (2) makes use of the _unseal lemmas because the instances are sealing. The use of unfold in (1) is not great because:

• If you have goals that involve multiple BIs, e.g., monPred I (iProp Σ), then you might unfold projections of the wrong BI. For example, calling monPred.unseal on something like ⎡ P ∗ Q ⎤ ∗ R will unfold both bi_seps, thus exposing a uPred_sep, i.e., uPred_sep P Q ∗ R i. It should only unfold the embed and the second bi_sep.
• The unfold tactic and rewrite / for records with primitive projections is buggy, see https://github.com/coq/coq/issues/5698

This MR provides an alternative. We lift the _unseal lemmas to the projections of the BI canonical structures/classes, solving both problems above.

Other changes:

• Restructure the monpred file to have all canonical/type class instances at a single place, instead of spread throughout the file
• Change the monpred unseal tactic to no longer unfold derived connectives. This is inconsistent with the unseal tactic for upred.
• Add an unseal tactic for siProp.