anchor.diff:      let hd, args = U.head_and_args rt in
       match (SS.compress hd).n, args with
       | Tm_fvar fv, [] when S.fv_eq_lid fv C.term_lid ->
  -        Some <| coerce_with env e lc S.t_term_view C.inspect [] []
  +        Some <| coerce_with env e lc S.t_term_view C.inspect [] [] S.mk_Total
       | _ ->
           None
   
  
positive.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 <| S.mk_Total ty) in
          let e = mk_Tm_app coercion [S.as_arg e] None e.pos in
          e, lc
      | None ->
  
negative.code:                 (ty : typ) // new result typ
                  (f : lident) // coercion
                  (us : universes) (eargs : args) // extra arguments to coertion
                  (mkcomp : term -> comp)
                  : term * lcomp =
      match Env.try_lookup_lid env f with
      | Some _ ->
  