anchor.diff:          | _ -> None)
        | _ -> None)
      | _ -> None
  -
   
   
   (************************************************************************************************************)
  
positive.code:             t, Env.conj_guard g1_env g2_env in
  
          let hd = {hd with sort=t} in
          let b = {binder_bv=hd;binder_qual=imp;binder_attrs=attrs} in
          let b_expected = ({binder_bv=hd_expected;binder_qual=imp';binder_attrs=attrs'}) in
          let env_b = push_binding env b in
          let subst = maybe_extend_subst subst b_expected (S.bv_to_name hd) in
  
negative.code:     let guard = TcUtil.close_guard_implicits env false bs guard in //TODO: this is a noop w.r.t scoping; remove it and the eager_subtyping flag
      let tfun_computed = U.arrow bs cbody in
      let e = U.abs bs body (Some (U.residual_comp_of_comp (dflt cbody c_opt))) in
  
      (*
       * AR: Check strictly_positive annotations on the binders, if any
       *
       *     To do so, we use the same routine as used for inductive types,
       *       after substituting the bv name with a fresh lid fv in the function body
       *)
      List.iter (fun b ->
        if U.has_attribute b.binder_attrs Const.binder_strictly_positive_attr
        then let r = TcUtil.name_strictly_positive_in_type env b.binder_bv body in
             if not r
             then raise_error (Error_InductiveTypeNotSatisfyPositivityCondition,
                    BU.format1 "Binder %s is marked strictly positive, but its use in the definition is not"
                                 (Print.binder_to_string b)) (S.range_of_bv b.binder_bv)
             else ()
        else ()) bs;
  
      (*
       * AR: there are three types in the code above now:
       *     topt : option<term> -- the original annotation
  