anchor.diff:  | _ -> failwith "Nested positive check, unhandled case"
   
   
  +let name_strictly_positive_in_type env bv t =
  +  let fv_lid = lid_of_str "__fv_lid_for_positivity_checking__" in
  +  let fv = S.tconst fv_lid in
  +  let t = SS.subst [NT (bv, fv)] t in
  +  ty_strictly_positive_in_type env fv_lid t (BU.mk_ref [])
  +
   //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
  
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 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
      b
  
    | Tm_app (_, _) ->
  
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));
  