val r_subst_of_rt_subst_elt (x: subst_elt) : FStar.Reflection.V2.subst_elt
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 r_subst_of_rt_subst_elt (x: subst_elt) : FStar.Reflection.V2.subst_elt
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
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.Naming.subst_elt Prims.nat Pulse.Syntax.Base.term FStar.Stubs.Syntax.Syntax.DT Pulse.Elaborate.Pure.elab_term Pulse.Syntax.Base.var FStar.Stubs.Syntax.Syntax.NT FStar.Reflection.Typing.var_as_namedv FStar.Stubs.Syntax.Syntax.NM FStar.Stubs.Syntax.Syntax.subst_elt
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)
val r_subst_of_rt_subst_elt (x: subst_elt) : FStar.Reflection.V2.subst_elt
x: Pulse.Syntax.Naming.subst_elt -> FStar.Stubs.Syntax.Syntax.subst_elt