feat: expand mapping functionailty in core

[LiamSchilling]

Mapping HVectors:

• defined fromMap', which is like toMap', except it maps FROM an HVector with a mapped index list instead of TO.
• defined castToMap and castFromMap for the special case where the transformation is id

Mapping valuations:

• defined toMap and fromMap for mapping valuations according to a transformation f' to and from contexts mapped by f
• defined castToMap and castFromMap for the special case where the transformation is id
• proved variable application lemmas

Mapping region signatures:

• defined abbreviations for operations on elements of region signatures
• defined mapElem abbreviation for mapping just those elements, as opposed to entire region signatures

Additionally:

• definitional equality lemma Expr.outContext_eq

[luisacicolini]

Hello @LiamSchilling, thank you for the PR! We'll look into it soon.