anchor.diff:          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_fvar _         -> 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
  
positive.code:             //open dbs
              let dbs = SS.open_binders dbs in
  
              //caller should normalize the term
              let ty_occurs_in (t:term) :bool = FStar.Util.set_mem lid (Free.fvars t) in
  
              let rec ty_strictly_positive_in (bsort:term) (env:env) :bool =
  
                let ty_nested_positive_in (ilid:lident) (args:args) (env:env) :bool =
                  let b, idatas = datacons_of_typ env ilid in
                  if not b then false
                  else
  
negative.code:                     | _                -> 0
                    in
                    
                    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
  