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:         tcs, datas
  
  
  let debug_log (env:env_t) (s:string) :unit = if Env.debug env <| Options.Other "Positivity" then BU.print_string ("Positivity::" ^ s ^ "\n") else ()
  
  //return true if ty occurs in the term
  let ty_occurs_in (ty_lid:lident) (t:term) :bool = FStar.Util.set_mem ty_lid (Free.fvars t)
  
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
  