anchor.diff:                  (match (FStar.Syntax.Subst.compress h').n with
                    | Tm_fvar fv when fv_eq_lid fv PC.list_lid ->
                        let arg_term = fst (List.hd args) in
  -                     "list", [mk_tac_embedding_path tcenv m arg_term], mk_tac_param_type arg_term, false
  +                     "list", [mk_tac_embedding_path tcenv m arg_term], mk_tac_param_type tcenv arg_term, false
                    | Tm_fvar fv when fv_eq_lid fv PC.option_lid ->
                        let arg_term = fst (List.hd args) in
  -                     "option", [mk_tac_embedding_path tcenv m arg_term], mk_tac_param_type arg_term, false
  +                     "option", [mk_tac_embedding_path tcenv m arg_term], mk_tac_param_type tcenv arg_term, false
                    | Tm_fvar fv when fv_eq_lid fv PC.tactic_lid ->
                        let arg_term = fst (List.hd args) in
  -                     "list", [mk_tac_embedding_path tcenv m arg_term], mk_tac_param_type arg_term, true
  +                     "list", [mk_tac_embedding_path tcenv m arg_term], mk_tac_param_type tcenv arg_term, true
                    | _ ->
                        raise_err (Fatal_CallNotImplemented, ("Embedding not defined for higher-order type " ^ (Print.term_to_string (FStar.Syntax.Subst.compress h'))))) in
               let hargs =
  
positive.code:         let args =
              [tac_fun] @
              (List.map (mk_tac_embedding_path tcenv Unembed) arg_types) @
              [mk_tac_embedding_path tcenv Embed t; mk_tac_param_type t; tac_lid_app; psc; str_to_name "args"] in
          let app = with_ty MLTY_Top <| MLE_App (h, List.map (with_ty MLTY_Top) args) in
          Some (MLE_Fun ([("psc", MLTY_Top); ("args", MLTY_Top)], app))
      with Errors.Error(Fatal_CallNotImplemented, msg, _)->
  
negative.code:            (match (FStar.Syntax.Subst.compress h').n with
              | Tm_fvar fv when fv_eq_lid fv PC.list_lid ->
                  let arg_term = fst (List.hd args) in
                  MLE_App (with_ty MLTY_Top (fstar_tc_common_prefix "t_list_of"), List.map (with_ty MLTY_Top) [mk_tac_param_type tcenv arg_term])
              | Tm_fvar fv when fv_eq_lid fv PC.option_lid ->
                  let arg_term = fst (List.hd args) in
                  MLE_App (with_ty MLTY_Top (fstar_tc_common_prefix "t_option_of"), List.map (with_ty MLTY_Top) [mk_tac_param_type tcenv arg_term] )
              | _ ->
                  raise_err (Fatal_CallNotImplemented, ("Type term not defined for higher-order type" ^ (Print.term_to_string (FStar.Syntax.Subst.compress h')))))
          | _ ->
              raise_err (Fatal_CallNotImplemented, "Impossible\n"))
       | _ when not unrefined ->
          // We failed to recognize the type, try unrefining (after unfolding).
          // This will make `nat` fall into the `int` case.
          let t = FStar.TypeChecker.Normalize.normalize
                      [FStar.TypeChecker.Normalize.UnfoldUntil FStar.Syntax.Syntax.Delta_constant]
                      tcenv
                      t
          in try_mk (FStar.Syntax.Util.unrefine t) true
       | _ ->
           raise_err (Fatal_CallNotImplemented, ("Type term not defined for " ^ (Print.term_to_string (FStar.Syntax.Subst.compress t))))
    in try_mk t false
  
  (* Except for the `tactic` type, which is handled specially, this assumes that functions for embedding/unembedding a type
     live in the same place and are named embed_x, unembed_x *)
  