Revert "Merge branch 'duplicable-type-class' into 'master'"

CHANGELOG.md

theories/base_logic/derived.v

theories/base_logic/lib/auth.v

theories/base_logic/lib/invariants.v

theories/base_logic/lib/own.v

theories/bi/big_op.v

theories/bi/derived_connectives.v

theories/bi/derived_laws.v

theories/bi/derived_laws_later.v

theories/bi/internal_eq.v

theories/bi/lib/fractional.v

theories/bi/plainly.v

theories/bi/telescopes.v

theories/proofmode/class_instances_later.v

theories/proofmode/environments.v

theories/proofmode/frame_instances.v