Axiomatizing frame functions to be injective

[marcoeilers]

Carbon internally uses the functions FrameFragment and FrameCombine both to frame functions and to model predicate snapshots, essentially equivalently to Silicon's XToSnap and SnapCombine.
However, currently, they are not axiomatized to be injective, even though they clearly could be.
Doing this has the advantage of giving us a way of framing heap information that's hidden inside predicates besides the existing known-folded-permission mechanism, which has the advantage of also working retroactively, fixing issues #355 and #259 and also #278.

The point is that during a predicate unfolding, Carbon emits an assumption like

assume UnfoldingHeap[null, P(x)] == FrameFragment(UnfoldingHeap[x, f]);

(for a predicate P containing only a permission to field f. If FrameFragment is known to be injective, this existing assumption suffices to get retroactive framing in cases like the ones shown in the issues.

This PR introduces inverse functions for both of the aforementioned functions and axioms that mark the functions as injective using the inverse functions.