anchor.diff:                      | _                -> 0
                     in
                     
  -                  let ty_nested_positive_in_d (dlid:lident) (env:env) :bool =
  +                  let ty_nested_positive_in (t:term') (env:env) :bool =
  +                    match t with
  +                    | Tm_app (t, args) ->
  +                      let fv = get_head_fvar_of_app_node t in
  +                      if Ident.lid_equals fv.fv_name.v ilid then true  //TODO: check that the ty does not appear in the indexes, don't understand that though
  +                      else false
  +                    | Tm_arrow (sbs, c) ->
  +                      fst (List.fold_left (fun (r, env) b ->
  +                             if not r then r, env
  +                             else
  +                             match (SS.compress (fst b).sort).n with
  +                             | Tm_app (t, args) ->
  +                               let fv = get_head_fvar_of_app_node t in
  +                               if Ident.lid_equals fv.fv_name.v ilid then true, push_binders env [b]  //TODO: check that the ty does not appear in the indexes
  +                               else (ty_strictly_positive_in (fst b).sort env, push_binders env [b])
  +                             | _ ->  ty_strictly_positive_in (fst b).sort env, push_binders env [b]
  +                           ) (true, env) sbs)  //TODO: also check c, c should be an I ... check ty does not occur in indexes
  +                    | _ -> failwith "Nested positive check, unhandled case"  //TODO: Type typed binders?
  +                  in
  +
  +                  let ty_nested_positive_in_dlid (dlid:lident) (env:env) :bool =
                       let _, dt = lookup_datacon env dlid in
  +                    let dt = N.normalize [N.Beta; N.Eager_unfolding; N.UnfoldUntil Delta_constant; N.Iota; N.Zeta; N.AllowUnboundUniverses] env dt in
                       //apply universe substitution to the datacon type
                       let dt = SS.subst usubst dt in
                       //open the type parameters of the inductive
  
positive.code:         let dt = SS.subst usubst dt in
  
          match (SS.compress dt).n with
            | Tm_fvar _         -> Util.print_string "This is the case of type with no argument, datacon also no arguments\n"; true  //TODO: my understanding is that this is the case where type has no arguments
            | Tm_arrow (dbs, _) ->
              //filter out the inductive type parameters, dbs are the remaining binders
              let dbs = snd (List.splitAt (List.length bs) dbs) in
  
negative.code:           | Sig_inductive_typ (lid, us, bs, _, _, _, _, _) -> lid, us, bs  //TODO: handle type indices
            | _                                           -> failwith "Impossible!"
        in
  
        let ty_occurs_in (t:term) :bool = FStar.Util.set_mem lid (Free.fvars t) in
  
        let ty_not_in_its_args (args:args) :bool = List.for_all (fun s -> not (ty_occurs_in s)) (List.map fst args) in
  
        let get_head_fvar_of_app_node (t:term) :fv =
          match (SS.compress t).n with
          | Tm_fvar fv      -> fv
          | Tm_uinst (t, _) ->
            (match t.n with
             | Tm_fvar fv   -> fv
             | _            -> failwith "Head node is a Tm_uinst, but Tm_uinst is not an fvar")
          | _               -> failwith "Head node is not an fvar or a Tm_uinst"
        in
  
        let usubst, us = SS.univ_var_opening us in
        //apply usubt to bs
        let bs = SS.subst_binders usubst bs in
  