anchor.diff:  
       else match Env.try_lookup_lid env ilid with
            | Some ((_, t), _) ->
  -           check_strictly_positive_argument ty_lid t args
  +           check_strictly_positive_argument env ty_lid t args unfolded
            | None ->
              debug_positivity env (fun () -> "Checking nested positivity, no attrs or type, return false");
              false
  
positive.code:  * This function checks that whereever ty_lid appears in the args,
   *   the corresponding parameter in t is marked strictly positive
   *)
  let check_strictly_positive_argument
    (ty_lid:lident)
    (t:typ)
    (args:args)
    : bool =
    let bs, _ = U.arrow_formals t in
    let rec aux (bs:binders) args : bool =
  
negative.code:       List.for_all (fun (arg, _) -> not (ty_occurs_in ty_lid arg)) args
      | b::bs, (arg, _)::args ->
        ((not (ty_occurs_in ty_lid arg)) ||
         (ty_strictly_positive_in_type env ty_lid arg unfolded &&
          U.has_attribute
            b.binder_attrs
            FStar.Parser.Const.binder_strictly_positive_attr))
        && aux bs args
    in
    aux bs args
  
  //check if ty_lid occurs strictly positively in some binder type btype
  and ty_strictly_positive_in_type env (ty_lid:lident) (btype:term) (unfolded:unfolded_memo_t) : bool =
    debug_positivity env (fun () -> "Checking strict positivity in type: " ^ (Print.term_to_string btype));
    //normalize the type to unfold any type abbreviations
    let btype = N.normalize
  