Cleanup following the BI and SBI merge

This MR cleans up all occurrences of sbi. Concretely, it performs the following changes:

• Rename bi.derived_laws_bi → bi.derived_laws and bi.derived_laws_sbi → bi.derived_laws_later.
• Reorganize bi.big_op file to remove sbi section.
• Reorganize proofmode.coq_tactics file to remove sbi section.
• Fine-grained split of proofmode.class_instances based on the structure of the bi folder. There are now files: class_instances, class_instances_later, class_instances_updates, class_instances_embedding, class_instances_plainly, class_instances_internal_eq.

This change should be backwards compatible, unless developments explicitly import "private" files.