Merge BI and SBI canonical structures

This MR flattens the BI hierarchy by merging the bi and sbi canonical structures. This gives significant performance benefits on developments that nest BI formers (e.g., use monPred). For, example it gives a performance gain of 37% overall on lambdarust-weak, with improvements for individual files up to 72%, see Iris issue #303. The concrete changes are as follows:

• The sbi canonical structure has been removed.
• The bi canonical structure contains the later modality. For non step-indexed BIs the later modality can simply be defined as the identity function, as the bi canonical structure does not require the later modality to be contractive, or to satisfy the Löb rule.
• There is a smart constructor bi_later_mixin_id that allows getting the later axioms for "free" if later is defined as the identity function.
• There is a separate class BiLöb, and a "free" instance of that class if the later modality is contractive. A BiLöb instance is required for the iLöb tactic, and for timeless instances of implication and wand.
• Since the sbi canonical structure has been removed, there is a separate type class BiInternalEq for BIs with a notion of internal equality. An instance of this class is needed for the iRewrite tactic and the various lemmas about internal equality.
• The class SbiEmbed has been removed and been replaced by classes BiEmbedLater and BiEmbedInternalEq.
• The class BiPlainly has been generalized to BIs without internal equality. As a consequence, there is a separate class BiPropExt for BIs with propositional extensionality (i.e., ■ (P ∗-∗ Q) ⊢ P ≡ Q).
• The class BiEmbedPlainly is a bi-entailment (i.e., ⎡■ P⎤ ⊣⊢ ■ ⎡P⎤ instead of ■ ⎡P⎤ ⊢ ⎡■ P⎤) as it has been generalized to BIs without a internal equality. In the past, the left-to-right direction was obtained for "free" using the rules of internal equality.

Some prior discussion points

• Should we keep the BiMixin and SbiMixin, or merge them?
  No longer relevant. SbiMixin has been renamed into BiLaterMixin.
• Should we keep the files derived_laws_bi and derived_laws_sbi, or merge them? These files are large, so maybe we should split them in a different way.
  Let's do that in a subsequent clean up MR.
• Does the class SbiEmbed still make sense? I expect that embeddings exist for which we not have ⎡▷ P⎤ ⊣⊢ ▷ ⎡P⎤, but maybe those are somewhat esoteric to justify the existence of this additional type class.
  No longer relevant. This class has been split up into BiEmbedLater and BiEmbedInternalEq.
• There are still some sections left that are called sbi_*. Should we merge those with other sections?
  Most of them have been removed, some that are left require more invasive changes to files. Let's do this in a separate cleanup MR.