anchor.diff:      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 env ty_lid b.binder_bv.sort unfolded, 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
  +        else begin
  +          //
  +          // AR: iterate over all the inductive type parameters,
  +          //     and see if they are marked strictly positive,
  +          //       and if so, they are indeed strictly positive in the
  +          //       data constructor binder type
  +          //
  +          (List.iter (fun {binder_bv=ty_bv; binder_attrs=ty_b_attrs} ->
  +             if U.has_attribute ty_b_attrs C.binder_strictly_positive_attr &&
  +                not (name_strictly_positive_in_type env ty_bv b.binder_bv.sort)
  +             then raise_error (Error_InductiveTypeNotSatisfyPositivityCondition,
  +                    BU.format1 "Binder %s is marked strictly positive, \
  +                                but its use in the definition is not"
  +                               (Print.bv_to_string ty_bv)) (S.range_of_bv ty_bv)) ty_bs);
  +
  +          //
  +          // AR: And now check that the inductive type itself is 
  +          //     strictly positive in this data constructor binder type
  +          //
  +          ty_strictly_positive_in_type env ty_lid b.binder_bv.sort unfolded,
  +          push_binders env [b]  //push the binder in the environment,
  +                                //we do some normalization, so better to keep env good
  +        end
  +      ) (true, env) dbs in
       b
   
     | Tm_app (_, _) ->
  
positive.code: | _ -> failwith "Nested positive check, unhandled case"
  
  
  //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 env (ty_lid:lident) (dlid:lident) (ty_bs:binders) (us:universes) (unfolded:unfolded_memo_t) : bool =
    //get the type of the data constructor
  
negative.code:   if Env.debug env <| Options.Other "Positivity"
    then BU.print_string ("Positivity::" ^ msg () ^ "\n")
  
  (*
   * We are checking for positive occurrences of ty_lid in a term
   *   (head args), and we know ty_lid occurs somewhere in args
   * In some env, we also have    env |- head : Tot t
   *
   * 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 =
      match bs, args with
      | _, [] -> true
      | [], _ ->
        List.for_all (fun (arg, _) -> not (ty_occurs_in ty_lid arg)) args
      | b::bs, (arg, _)::args ->
        ((not (ty_occurs_in ty_lid arg)) ||
         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
  let rec 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));
  