anchor.diff:  
       match (U.un_uinst head).n, args with
       | Tm_fvar fv, [] when S.fv_eq_lid fv C.bool_lid && is_type t ->
  -        coerce_with env e lc U.ktype0 C.b2t_lid [] []
  +        coerce_with env e lc U.ktype0 C.b2t_lid [] [] S.mk_Total
   
   
       | Tm_fvar fv, [] when S.fv_eq_lid fv C.term_lid && is_t_term_view t ->
  -        coerce_with env e lc S.t_term_view C.inspect [] []
  +        coerce_with env e lc S.t_term_view C.inspect [] [] S.mk_Total
   
       | Tm_fvar fv, [] when S.fv_eq_lid fv C.term_view_lid && is_t_term t ->
  -        coerce_with env e lc S.t_term C.pack [] []
  +        coerce_with env e lc S.t_term C.pack [] [] S.mk_Total
   
       | Tm_fvar fv, [] when S.fv_eq_lid fv C.binder_lid && is_t_term t ->
  -        coerce_with env e lc S.t_term C.binder_to_term [] []
  +        coerce_with env e lc S.t_term C.binder_to_term [] [] S.mk_Tac
   
   
       | _ when is_erased env t res_typ ->
  -        coerce_with env e lc t C.reveal [env.universe_of env t] [S.iarg t]
  +        coerce_with env e lc t C.reveal [env.universe_of env t] [S.iarg t] S.mk_GTotal
   
       | _ when is_erased env res_typ t ->
  -        coerce_with env e lc t C.hide [env.universe_of env res_typ] [S.iarg res_typ]
  +        coerce_with env e lc t C.hide [env.universe_of env res_typ] [S.iarg res_typ] S.mk_Total
  +
   
       | _ ->
         e, lc
  
positive.code:                 (ty : typ) // new result typ
                  (f : lident) // coercion
                  (us : universes) (eargs : args) // extra arguments to coertion
                  : term * lcomp =
      match Env.try_lookup_lid env f with
      | Some _ ->
  
negative.code:         let coercion = S.fvar (Ident.set_lid_range f e.pos) (Delta_constant_at_level 1) None in
          let coercion = S.mk_Tm_uinst coercion us in
          let coercion = U.mk_app coercion eargs in
          let lc = bind e.pos env (Some e) lc (None, U.lcomp_of_comp <| mkcomp ty) in
          let e = mk_Tm_app coercion [S.as_arg e] None e.pos in
          e, lc
      | None ->
  