+Note [The Solver Invariant]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We always add Givens first. So you might think that the solver has
+the invariant
+
+ If the work-item is Given,
+ then the inert item must Given
+
+But this isn't quite true. Suppose we have,
+ c1: [W] beta ~ [alpha], c2 : [W] blah, c3 :[W] alpha ~ Int
+After processing the first two, we get
+ c1: [G] beta ~ [alpha], c2 : [W] blah
+Now, c3 does not interact with the the given c1, so when we spontaneously
+solve c3, we must re-react it with the inert set. So we can attempt a
+reaction between inert c2 [W] and work-item c3 [G].
+
+It *is* true that [Solver Invariant]
+ If the work-item is Given,
+ AND there is a reaction
+ then the inert item must Given
+or, equivalently,
+ If the work-item is Given,
+ and the inert item is Wanted/Derived
+ then there is no reaction
+