Make lifetimesThatCouldProve more precise

[eddywestbrook]

The main focus of this PR is to make the lifetimesThatCouldProve function more precise. The goal of lifetimesThatCouldProve is to determine all the lifetimes that might need to be ended in order to prove a given goal in the implication prover. The implication prover then tries ending each of these in turn to see which ones need to be ended in order to succeed.

The old approach to lifetimesThatCouldProve was to simply test if ending a lifetime l would give back permissions on any variable x that we are trying to prove permissions for. The old version of this function turned out to have three problems:

1. It would return a lifetime l in cases where the specific permissions for x given back by ending l wasn't actually needed, giving too many false positives; and
2. It would not consider other variables y for which we currently have permissions like x:ptr((W,0) |-> eq(y)) whose permissions we do need to prove permissions on x.
3. It didn't take into account that the implication prover should try to end "smaller" lifetimes first, before trying "bigger" lifetimes that contain those smaller ones.
   This PR addresses these problems by redefining lifetimesThatCouldProve to take these issues into account.

As part of this changes, this PR also makes the following changes:

• extImplState, withExtVarsM, and related functions no longer need a KnownRepr TypeRepr a for the type of the new evars added to the state, but now instead only need a `TypeRepr a;
• The SomeMbPerm and MbRangeForLLVMType types now only need a CruCtx instead of a KnownCruCtx;
• A problematic case for recombinePerm was commented out; and
• A non-exhaustive pattern-matching error in SAWTranslation.hs was fixed.

[m-yac]

LGTM. I like the comments you added to lifetimesThatCouldProve and proveVarAtomicImpl!