anchor.diff:  //dlid is a data constructor of ilid, args are the arguments of the ilid application, num_ibs is the # of type parameters of ilid
   //us are the universes, see the exaplanation on ty_nested_positive_in_inductive
   and ty_nested_positive_in_dlid (ty_lid:lident) (dlid:lident) (ilid:lident) (us:universes) (args:args) (num_ibs:int) (unfolded:unfolded_memo_t) (env:env_t) :bool =
  -  debug_log env ("Checking nested positivity in data constructor " ^ dlid.str ^ " of the inductive " ^ ilid.str);
  +  debug_log env (fun () -> "Checking nested positivity in data constructor " ^ dlid.str ^ " of the inductive " ^ ilid.str);
     //get the type of the data constructor
     let univ_unif_vars, dt = lookup_datacon env dlid in
     //lookup_datacon instantiates the universes of dlid with unification variables
  
positive.code:   //normalize it, TODO: as before steps?
    let dt = N.normalize [Env.Beta; Env.Eager_unfolding; Env.UnfoldUntil delta_constant; Env.Iota; Env.Zeta; Env.AllowUnboundUniverses] env dt in
  
    debug_log env ("Checking nested positivity in the data constructor type: " ^ (PP.term_to_string dt));
    match (SS.compress dt).n with
    | Tm_arrow (dbs, c) ->  //if the data construtor type is an arrow, we need to substitute the args for type parameters of ilid
      //so ibs are the type parameters of inductive, that we would substitute with args, dbs are remaining binders of the data constructor
      debug_log env ("Checked nested positivity in Tm_arrow data constructor type");
      let ibs, dbs = List.splitAt num_ibs dbs in
      //open ibs
      let ibs = SS.open_binders ibs in
  
negative.code: //us are the universes that the inductive ilid's data constructors can be instantiated with if needed, these us come from the application of ilid that called this function
  //TODO: change the name of the function to reflect this behavior
  and ty_nested_positive_in_inductive (ty_lid:lident) (ilid:lident) (us:universes) (args:args) (unfolded:unfolded_memo_t) (env:env_t) :bool =
    debug_log env (fun () -> "Checking nested positivity in the inductive " ^ ilid.str ^ " applied to arguments: " ^ (PP.args_to_string args));
    let b, idatas = datacons_of_typ env ilid in
    //if ilid is not an inductive, return false
    if not b then begin
  