anchor.diff:      BU.print1 "%s ..." (BU.string_of_int i);
       FStar.Main.process_args () |> ignore; //set options
       BU.print2 "Unify %s\nand %s\n" (FStar.Syntax.Print.term_to_string x) (FStar.Syntax.Print.term_to_string y);
  -    let g = Rel.teq (tcenv()) x y |> Rel.solve_deferred_constraints (tcenv()) in
  +    let g = Rel.teq (tcenv()) x y |> Rel.solve_deferred_constraints (tcenv()) |> Rel.simplify_guard (tcenv()) in
       guard_eq i g.guard_f g';
       check();
       Options.init()    //reset them; exceptions are fatal, so don't worry about resetting them in case guard_eq fails
  
positive.code:         tm1, tm2
      in
  
      unify 13 tm1 tm2 (NonTrivial (tc "Prims.l_True"));
  
      let tm1, tm2 =
          let int_typ = tc "int" in
  
negative.code:     unify 4 id id' Trivial; //(NonTrivial (pars "True /\ (forall x. True)"));
  
      //alpha equivalence 2
      unify 5 (tc "fun x y -> x")
              (tc "fun a b -> a")
              Trivial;
  