Language.Fixpoint.Solver.Sanitize
Transform FInfo to enforce invariants
sanitize
Sorts for each Symbol (move elsewhere)
symbolEnv
Remove substitutions K[x := e] where
x
is not in dom(K)
dropDeadSubsts