val return_post_with_eq (u: universe) (a e p: term) (x: var) : term
let return_post_with_eq (u:universe) (a:term) (e:term) (p:term) (x:var) : term =
  let x_tm = RT.var_as_term x in
  let eq2_tm = mk_eq2 u a x_tm e in
  let p_app_x = pack_ln (Tv_App p (x_tm, Q_Explicit)) in  
  let star_tm = mk_star p_app_x (mk_pure eq2_tm) in
  mk_abs a Q_Explicit (RT.subst_term star_tm [ RT.ND x 0 ])
val return_post_with_eq (u: universe) (a e p: term) (x: var) : term
let return_post_with_eq (u: universe) (a e p: term) (x: var) : term =
let x_tm = RT.var_as_term x in
let eq2_tm = mk_eq2 u a x_tm e in
let p_app_x = pack_ln (Tv_App p (x_tm, Q_Explicit)) in
let star_tm = mk_star p_app_x (mk_pure eq2_tm) in
mk_abs a Q_Explicit (RT.subst_term star_tm [RT.ND x 0])
Pulse.Steel.Wrapper.Typing.fsti.checked
Pulse.Reflection.Util.fst.checked prims.fst.checked FStar.Reflection.V2.fst.checked FStar.Reflection.Typing.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Pulse.Steel.Wrapper.Typing.fsti
FStar.Reflection.Types.universe FStar.Reflection.Types.term FStar.Reflection.V2.Data.var Pulse.Reflection.Util.mk_abs FStar.Reflection.V2.Data.Q_Explicit FStar.Reflection.Typing.subst_term Prims.Cons FStar.Reflection.Typing.subst_elt FStar.Reflection.Typing.ND Prims.Nil Pulse.Reflection.Util.mk_star Pulse.Reflection.Util.mk_pure FStar.Reflection.V2.Builtins.pack_ln FStar.Reflection.V2.Data.Tv_App FStar.Pervasives.Native.Mktuple2 FStar.Reflection.V2.Data.aqualv Pulse.Reflection.Util.mk_eq2 FStar.Reflection.Typing.var_as_term
module Pulse.Steel.Wrapper.Typing

open FStar.Reflection.V2
open Pulse.Reflection.Util

module RT = FStar.Reflection.Typing
val return_post_with_eq (u: universe) (a e p: term) (x: var) : term

    u5: FStar.Reflection.Types.universe ->
    a: FStar.Reflection.Types.term ->
    e: FStar.Reflection.Types.term ->
    p: FStar.Reflection.Types.term ->
    x: FStar.Reflection.V2.Data.var
  -> FStar.Reflection.Types.term