Merge branch 'ralf/ra-docs' into 'master'

docs/heap_lang.md

docs/proof_guide.md

docs/resource_algebras.md

tests/one_shot.v

tests/one_shot_once.v

tests/proofmode_iris.v

theories/base_logic/derived.v

theories/base_logic/lib/auth.v

theories/base_logic/lib/boxes.v

theories/base_logic/lib/cancelable_invariants.v

theories/base_logic/lib/fancy_updates.v

theories/base_logic/lib/gen_heap.v

theories/base_logic/lib/ghost_var.v

theories/base_logic/lib/invariants.v

theories/base_logic/lib/mnat.v

theories/base_logic/lib/na_invariants.v

theories/base_logic/lib/saved_prop.v

theories/base_logic/lib/sts.v

theories/base_logic/lib/wsat.v

theories/base_logic/upred.v