anchor.diff:       match (SS.compress btype).n with
        | Tm_app (t, args) ->  //the binder type is an application
          //get the head node fv, try_get_fv would fail if it's not an fv
  -       let fv, us = try_get_fv t in
  -       //if it's same as ty_lid, then check that ty_lid does not occur in the arguments
  -       if Ident.lid_equals fv.fv_name.v ty_lid then
  -         let _ = debug_log env (fun () -> "Checking strict positivity in the Tm_app node where head lid is ty itself, checking that ty does not occur in the arguments") in
  -         List.for_all (fun (t, _) -> not (ty_occurs_in ty_lid t)) args
  -         //else it must be another inductive type, and we would check nested positivity, ty_nested_positive fails if fv is not another inductive
  -         //that case could arise when, for example, it's a type constructor that we could not unfold in normalization
  +       let fv_us_opt = try_get_fv t in
  +       if fv_us_opt |> is_none then true  //head is not an fv, ok
          else
  -         let _ = debug_log 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
  +         let fv, us = fv_us_opt |> must in
  +         //if it's same as ty_lid, then check that ty_lid does not occur in the arguments
  +         if Ident.lid_equals fv.fv_name.v ty_lid then
  +           let _ = debug_log env (fun () -> "Checking strict positivity in the Tm_app node where head lid is ty itself, checking that ty does not occur in the arguments") in
  +           List.for_all (fun (t, _) -> not (ty_occurs_in ty_lid t)) args
  +           //else it must be another inductive type, and we would check nested positivity, ty_nested_positive fails if fv is not another inductive
  +           //that case could arise when, for example, it's a type constructor that we could not unfold in normalization
  +         else
  +           let _ = debug_log 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
        | Tm_arrow (sbs, c) ->  //binder type is an arrow type
          debug_log env (fun () -> "Checking strict positivity in Tm_arrow");
          let check_comp =
  
positive.code: 
  //this function is called during the positivity check, when we have a binder type that is a Tm_app, and t is the head node of Tm_app
  //it tries to get fvar from this t, since the type is already normalized, other cases should have been handled
  let try_get_fv (t:term) :(fv * universes) =
  match (SS.compress t).n with
  | Tm_fvar fv       -> fv, []
  | Tm_uinst (t, us) ->
      (match t.n with
      | Tm_fvar fv   -> fv, us
      | _            -> failwith "Node is a Tm_uinst, but Tm_uinst is not an fvar")
  | _                -> failwith "Node is not an fvar or a Tm_uinst"
  
  type unfolded_memo_elt = list<(lident * args)>
  type unfolded_memo_t = ref<unfolded_memo_elt>
  
negative.code:   | Tm_app (t, args) ->
      //if it's an application node, it must be ilid directly
      debug_log env (fun () -> "Checking nested positivity in an Tm_app node, which is expected to be the ilid itself");
      let fv, _ = try_get_fv t |> must in
      if Ident.lid_equals fv.fv_name.v ilid then true  //TODO: in this case Coq manual says we should check for indexes
      else failwith "Impossible, expected the type to be ilid"
    | Tm_arrow (sbs, c) ->
  