anchor.diff:     that must hold for U. It is build from subtyping constraints of the form U <: t.
      We call q* a multiplicative slack variable.
   
  -   Subtyping constraints involving unification variables and refinement formulas introduce 
  -   and propagate slack variables in a manner that ensures that the subtyping constraints are satisfiable, 
  -   given the validity of a logical guard.
  -
  -   At the top-level of a derivation, all the remaining uninstantiated slack variables are collected. 
  -   Every positive variable p+ is instantiated to \xs.False
  -   Every negative variable q* is instantiated to \xs.True
  -
  -   An invariant of the system is, given the validity of the logical constraints emitted, the 
  -   lower bound of the system always implies the upper bound.
  -
      For readability, we will write a slack formula as
      
             Lower(F, p xs) /\ Upper(G, q xs)
      
  +   Subtyping constraints involving unification variables and refinement formulas introduce 
  +   and propagate slack variables in a manner that ensures that the subtyping constraints are satisfiable, 
  +   given the validity of a logical guard.
  +
  +   At the top-level of a derivation, all the remaining uninstantiated slack variables are collected. 
  +   Every additive variable p+ is instantiated to \xs.False
  +   Every multiplicative variable q* is instantiated to \xs.True
  +
  +   An invariant of the system is, given the validity of the logical constraints emitted, the 
  +   lower bound of the system always implies the upper bound.
  +
      
   1. Slack-intro-T-flex: Given a subtyping problem, with a uvar on the right:
              
  
positive.code: 
        x:t1{Lower(phi1, p1 xs) /\ Upper(psi1, q1 xs)} <: y:t2{Lower(phi2, p2 xs) /\ Upper(psi2, q2 xs)}
  
     1. t1 <: t2
  
     2 a. p1 = \xs. phi2 \/ p xs
     2 b. p2 = \xs. phi1 \/ p xs
  
     3 a. q1 = \xs. psi2 /\ q xs
     3 b. q2 = \xs. psi1 /\ q xs
  
     4 a. phi1 ==> psi2
     4 b. phi2 ==> psi1
  
  
  
  3 a. Slack-elim-L-pos: Given
              x:t{Pos(phi \/ slack x)}  <: x:t{phi'} 
         where phi' may or may not have slack
                 
         Solve by:
              slack = \x. Neg(phi' /\ slack' x) 
  
         And producing the logical constraint:
              forall x. phi x ==> phi' x
  
         Intuitively, by flipping the polarity of the slack and guarding it with phi', 
         we ensure that any further weakening instantiations of the slack cannot weaken it 
         beyond the desired bound phi'.
  
  3 b. Slack-elim-L-neg: Given
              x:t{Neg(phi \/ (psi /\ slack x))}  <: x:t{phi'} 
         where phi' may or may not have slack
                 
         Solve by:
              slack = \x. Neg(phi' /\ slack' x) 
  
         And producing the logical constraint:
              forall x. phi x ==> phi' x
  
  4. Slack-reintro-R: Given
             x:t{phi} <: x:t{slack x \/ phi'}
         where phi does not have slack
  
         Solve by setting
             slack = \x. slack' x \/ phi x
         for fresh slack'
  
  5. No-Slack-L: Given
        
         u <: t
  
     Solve it by setting u = t
  
     No point in leaving slack on the LHS, since t is a lower-bound anyway
  
  We carry all slack variables to the top-level. After solving all constraints,
  if there are any remaining slack variables, we set them all to \xs.False.
  
  Note, the case where both side have slack, is covered by case 3:
         Consider:
             x:t{slack1 x \/ phi1} <: x:t2{slack2 \/ phi2}
          
         Solve by:
             slack1 = \x. slack2 x \/ phi2
  
         And 
             forall x. phi1 x ==> (slack2 x \/ phi2 x) *)
  
  
  (* 
    A refinement formula phi may include a slack variable
  
negative.code: 
      where t' has no non-trivial super types.
      
      Then set: 
              u = \xs. x:t'{Lower(phi x, p x) /\ Upper(True /\ q x)})
   
      i.e., solve it by imitating the rhs, while introducing a slack formula, 
      recording phi as a lower bound.
  
  2. Slack-intro-fun-flex: Given 
  