anchor.diff:      debug_log env (fun () -> "Checking nested positivity in the unfolded data constructor binders as: " ^ (PP.binders_to_string "; " dbs) ^ ", and c: " ^ (PP.comp_to_string c));
       ty_nested_positive_in_type ty_lid (Tm_arrow (dbs, c)) ilid num_ibs unfolded env
     | _ ->
  +    //AR: TODO: 04/21: may be this should be an error since data constructor type is not an arrow?
       debug_log env (fun () -> "Checking nested positivity in the data constructor type that is not an arrow");
  -    ty_nested_positive_in_type ty_lid (SS.compress dt).n ilid num_ibs unfolded env  //in this case, we don't have anything to substitute, simply check
  +    ty_nested_positive_in_type ty_lid (SS.compress dt).n ilid num_ibs unfolded env //in this case, we don't have anything to substitute, simply check
   
   //t is some data constructor type of ilid, after ilid type parameters have been substituted
   and ty_nested_positive_in_type (ty_lid:lident) (t:term') (ilid:lident) (num_ibs:int) (unfolded:unfolded_memo_t) (env:env_t) :bool =
  
positive.code:      | U_unif u'' -> UF.univ_change u'' u
       | _          -> failwith "Impossible! Expected universe unification variables") univ_unif_vars us);
  
    //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 (fun () -> "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
  
negative.code: //check if ty_lid occurs strictly positively in some binder type btype
  let rec ty_strictly_positive_in_type (ty_lid:lident) (btype:term) (unfolded:unfolded_memo_t) (env:env_t) :bool =
    debug_log env (fun () -> "Checking strict positivity in type: " ^ (PP.term_to_string btype));
    //normalize the type to unfold any type abbreviations
    let btype = N.normalize
      [Env.Beta;
       Env.HNF;
       Env.Weak;
       Env.UnfoldUntil delta_constant;
       Env.Iota;
       Env.ForExtraction;
       Env.Unascribe;
       Env.AllowUnboundUniverses] env btype in
    debug_log env (fun () -> "Checking strict positivity in type, after normalization: " ^ (PP.term_to_string btype));
    not (ty_occurs_in ty_lid btype) ||  //true if ty does not occur in btype
      (debug_log env (fun () -> "ty does occur in this type, pressing ahead");
  