Documentation improvements and cleanup

This MR contains a few changes:

• move the vec case study to case_studies and integrate it into CI
• add a small tutorial.md document giving a tutorial on how to use RefinedRust
• add a small paper_mapping.md document describing how stuff from the RefinedRust paper maps to the code
• fix some issues with ADT shims

case_studies/extra_proofs/minivec/dune

-; Generated by [refinedrust], do not edit.
 (coq.theory
 (flags -w -notation-overridden -w -redundant-canonical-projection)
-(name refinedrust.examples.minivec_patched)
+(name refinedrust.extra_proofs.minivec)
 (theories stdpp iris Ltac2 Equations RecordUpdate lrust caesium lithium refinedrust))