let subst_host_term' (t:host_term) (ss:subst) =
  R2.subst_term (L.map r_subst_of_rt_subst_elt ss) t
let subst_host_term' (t: host_term) (ss: subst) =
R2.subst_term (L.map r_subst_of_rt_subst_elt ss) t
Pulse.Syntax.Naming.fst.checked
Pulse.Syntax.Pure.fst.checked Pulse.Syntax.Base.fsti.checked Pulse.RuntimeUtils.fsti.checked Pulse.Elaborate.Pure.fst.checked prims.fst.checked FStar.Set.fsti.checked FStar.Reflection.V2.fst.checked FStar.Reflection.Typing.Builtins.fsti.checked FStar.Reflection.Typing.fsti.checked FStar.Reflection.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Pulse.Syntax.Naming.fst
Pulse.Syntax.Base.host_term Pulse.Syntax.Naming.subst FStar.Reflection.V2.Builtins.subst_term FStar.List.Tot.Base.map Pulse.Syntax.Naming.subst_elt FStar.Stubs.Syntax.Syntax.subst_elt Pulse.Syntax.Naming.r_subst_of_rt_subst_elt FStar.Reflection.Types.term
module Pulse.Syntax.Naming
module RTB = FStar.Reflection.Typing.Builtins
module RT = FStar.Reflection.Typing
module R = FStar.Reflection
open FStar.List.Tot
module E = Pulse.Elaborate.Pure
open Pulse.Syntax.Base
module U = Pulse.Syntax.Pure
module R2 = FStar.Reflection.V2
module RU = Pulse.RuntimeUtils
let r_subst_of_rt_subst_elt (x:subst_elt)
  : FStar.Reflection.V2.subst_elt
  = match x with
    | DT i t -> R2.DT i (E.elab_term t)
    | NT x t -> R2.NT (RT.var_as_namedv x) (E.elab_term t) 
    | ND x i -> R2.NM (RT.var_as_namedv x) i
val subst_host_term' : t: Pulse.Syntax.Base.host_term -> ss: Pulse.Syntax.Naming.subst -> FStar.Reflection.Types.term
t: Pulse.Syntax.Base.host_term -> ss: Pulse.Syntax.Naming.subst -> FStar.Reflection.Types.term