anchor.diff:             //that case could arise when, for example, it's a type constructor that we could not unfold in normalization
            else
              let _ = debug_positivity env (fun () -> "Checking strict positivity in the Tm_app node, head lid is not ty, so checking nested positivity") in
  -           ty_nested_positive_in_inductive ty_lid fv.fv_name.v us args unfolded env
  +           ty_nested_positive_in_inductive env ty_lid fv.fv_name.v us args unfolded
  +
        | Tm_arrow (sbs, c) ->  //binder type is an arrow type
          debug_positivity env (fun () -> "Checking strict positivity in Tm_arrow");
          let check_comp =
  
positive.code:     let b, _ =
        List.fold_left (fun (r, env) b ->
          if not r then r, env  //if we have already found some binder that does not satisfy the condition, short circuit
          else ty_strictly_positive_in_type ty_lid b.binder_bv.sort unfolded env, push_binders env [b]  //push the binder in the environment, we do some normalization, so might be better to keep env good
        ) (true, env) dbs
      in
      b
    | Tm_app (_, _) ->
      debug_positivity env (fun () -> "Data constructor type is a Tm_app, so returning true");
      true  //if the data constructor type is a simple app, it must be t ..., and we already don't allow t (t ..), so nothing to check here
    | Tm_uinst (t, univs) ->
      debug_positivity env (fun () -> "Data constructor type is a Tm_uinst, so recursing in the base type");
      ty_strictly_positive_in_type ty_lid t unfolded env
    | _ -> failwith "Unexpected data constructor type when checking positivity"
  
  let check_positivity (env:env_t) (ty:sigelt) :bool =
    //memo table, memoizes the Tm_app nodes for inductives that we have already unfolded
  
negative.code:     (debug_positivity env (fun () -> "ty does occur in this type, pressing ahead");
       match (SS.compress btype).n with
       | Tm_app (t, args) ->  //the binder type is an application
         //get the head node fv
         let fv_us_opt = try_get_fv t in
         if fv_us_opt |> is_none then true  //head is not an fv, ok
         else
  