anchor.diff:    | Tm_app({n=Tm_constant Const_range_of}, [(e, None)]) ->
       let e, c, g = tc_term (fst <| Env.clear_expected_typ env) e in
       let head, _ = U.head_and_args top in
  -    mk (Tm_app (head, [(e, None)])) None top.pos, (Util.lcomp_of_comp <| mk_Total (tabbrev Const.range_lid)), g
  +    mk (Tm_app (head, [(e, None)])) None top.pos, (U.lcomp_of_comp <| mk_Total (tabbrev Const.range_lid)), g
   
     | Tm_app({n=Tm_constant Const_set_range_of}, (t, None)::(r, None)::[]) ->
       let head, _ = U.head_and_args top in
  
positive.code:       if not (Env.should_verify env)
        then U.t_true
        else (* 6 (a) *)
            let rec build_branch_guard scrutinee_tm pat_exp : list<typ> =
              let discriminate scrutinee_tm f =
                  let is_induc, datacons = Env.datacons_of_typ env (Env.typ_of_datacon env f.v) in
                  (* Why the `not is_induc`? We may be checking an exception pattern. See issue #1535. *)
  
negative.code: open FStar.Dyn
  open FStar.TypeChecker.Rel
  open FStar.TypeChecker.Common
  
  module S  = FStar.Syntax.Syntax
  module SS = FStar.Syntax.Subst
  module N  = FStar.TypeChecker.Normalize
  