anchor.diff:  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_positivity env (fun () -> "Checking nested positivity in data constructor " ^ (string_of_lid dlid) ^ " of the inductive " ^ (string_of_lid ilid));
     //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
  -  //we should unify the universe variables with us, us are the universes that the ilid fvar was instantiated with
  -  (List.iter2 (fun u' u -> match u' with
  -     | U_unif u'' -> UF.univ_change u'' u
  -     | _          -> failwith "Impossible! Expected universe unification variables") univ_unif_vars us);
  +    let dt =
  +    match Env.try_lookup_and_inst_lid env us dlid with
  +    | Some (t, _) -> t
  +    | None -> raise_error (Errors.Error_InductiveTypeNotSatisfyPositivityCondition,
  +               BU.format1 "Error looking up data constructor %s when checking positivity"
  +                 (string_of_lid dlid)) (range_of_lid ty_lid) in
   
     debug_positivity env (fun () -> "Checking nested positivity in the data constructor type: " ^ (Print.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
  
positive.code: 
  
  //ty_bs are the opended type parameters of the inductive, and ty_usubst is the universe substitution, again from the ty_lid type
  let ty_positive_in_datacon (ty_lid:lident) (dlid:lident) (ty_bs:binders) (us:universes) (unfolded:unfolded_memo_t) (env:env) :bool =
    //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
    //we should unify the universe variables with us, us are the universes that the ilid fvar was instantiated with
    (List.iter2 (fun u' u -> match u' with
       | U_unif u'' -> UF.univ_change u'' u
       | _          -> failwith "Impossible! Expected universe unification variables") univ_unif_vars us);
  
    debug_positivity env (fun () -> "Checking data constructor type: " ^ (Print.term_to_string dt));
    match (SS.compress dt).n with
    | Tm_fvar _ ->
      debug_positivity env (fun () -> "Data constructor type is simply an fvar, returning true");
      true  //if the dataconstructor type is simply an fvar, should be an inductive with no params, no indexes, and no binders in data constructor type
    | Tm_arrow (dbs, _) ->  //TODO: we should check the computation type is not of the form t (t a), but then typechecker already rejects this type
      //filter out the inductive type parameters, dbs are the remaining binders
      let dbs = snd (List.splitAt (List.length ty_bs) dbs) in
  
negative.code:   let ty_bs = SS.subst_binders ty_usubst ty_bs in
    let ty_bs = SS.open_binders ty_bs in
  
    List.for_all (fun d ->
      ty_positive_in_datacon
        env
        ty_lid
        d
        ty_bs
        (List.map U_name ty_us)
        unfolded_inductives) (snd (datacons_of_typ env ty_lid))
  
  let name_strictly_positive_in_type env bv t =
    let fv_lid = lid_of_str "__fv_lid_for_positivity_checking__" in
    let fv = S.tconst fv_lid in
    let t = SS.subst [NT (bv, fv)] t in
    ty_strictly_positive_in_type env fv_lid t (BU.mk_ref [])
  
  (* Special-casing the check for exceptions, the single open inductive type we handle. *)
  let check_exn_positivity (env:env_t) (data_ctor_lid:lid) : bool =
    //memo table, memoizes the Tm_app nodes for inductives that we have already unfolded
    let unfolded_inductives = BU.mk_ref [] in
    ty_positive_in_datacon env C.exn_lid data_ctor_lid [] []  unfolded_inductives
  