Remove LEM's global context

[arthurpaulino]

We should use purely functional data structures to handle LEM context in a way that isolates what happens on different logical branches/paths. This would allow us to nuke all the "deconflict" complexity.

This simplification can actually enable further improvements with potential performance gains. For example, we would be able to generate (partial) witnesses for each match/if arm in parallel. Right now, we need to do it sequentially because the global context is tied by mutability.