val return_stt_noeq_comp (u: universe) (a x p: term) : term
let return_stt_noeq_comp (u:universe) (a:term) (x:term) (p:term) : term =
  mk_stt_comp u a (pack_ln (Tv_App p (x, Q_Explicit))) p
val return_stt_noeq_comp (u: universe) (a x p: term) : term
let return_stt_noeq_comp (u: universe) (a x p: term) : term =
mk_stt_comp u a (pack_ln (Tv_App p (x, Q_Explicit))) p
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 Pulse.Reflection.Util.mk_stt_comp FStar.Reflection.V2.Builtins.pack_ln FStar.Reflection.V2.Data.Tv_App FStar.Pervasives.Native.Mktuple2 FStar.Reflection.V2.Data.aqualv FStar.Reflection.V2.Data.Q_Explicit
module Pulse.Steel.Wrapper.Typing

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

module RT = FStar.Reflection.Typing

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 ])

let return_stt_comp (u:universe) (a:term) (e:term) (p:term) (x:var) : term =
  mk_stt_comp u a
    (pack_ln (Tv_App p (e, Q_Explicit)))
    (return_post_with_eq u a e p x)

val return_stt_typing
  (#g:env)
  (#u:universe)
  (#a:term)
  (#e:term)
  (#p:term)
  (x:var{None? (RT.lookup_bvar g x)})
  (a_typing:RT.tot_typing g a (pack_ln (Tv_Type u)))
  (e_typing:RT.tot_typing g e a)
  (p_typing:RT.tot_typing g p (mk_arrow (a, Q_Explicit) vprop_tm))

  : GTot (RT.tot_typing g
            (mk_stt_return u a e p)
            (return_stt_comp u a e p x))
val return_stt_noeq_comp (u: universe) (a x p: term) : term

    u14: FStar.Reflection.Types.universe ->
    a: FStar.Reflection.Types.term ->
    x: FStar.Reflection.Types.term ->
    p: FStar.Reflection.Types.term
  -> FStar.Reflection.Types.term