anchor.diff:   | UnivArgs of list<universe> * Range.range
    | MemoLazy of memo<(env * term)>
    | Match    of env * branches * Range.range
  - | Abs      of env * binders * env * option<lcomp> * Range.range
  + | Abs      of env * binders * env * option<lcomp> * Range.range //the second env is the first one extended with the binders, for reducing the option<lcomp>
    | App      of term * aqual * Range.range
    | Meta     of S.metadata * Range.range
   
  
positive.code: type cfg = {
      steps: steps;
      tcenv: Env.env;
      delta_level: Env.delta_level
  }
  
  type branches = list<(pat * option<term> * term)> 
  
negative.code:   | UnfoldUntil of S.delta_depth
    | Beta            
    | BetaUVars
    | Simplify        //Simplifies some basic logical tautologies: not part of definitional equality!
    | EraseUniverses
    | AllowUnboundUniverses //we erase universes as we encode to SMT; so, sometimes when printing, it's ok to have some unbound universe variables
    //remove the rest?
  