Some more proof refactoring to get soundness working again

Changed one of the types in the type soundness invariant from a list of
pairs to a finite map.