val stc_soundness
  (#g:stt_env)
  (#st:st_comp)
  (d_st:st_comp_typing g st)
  
  : GTot (RT.tot_typing ( elab_env g)
                        (elab_term st.res)
                        (RT.tm_type st.u) &
          RT.tot_typing (elab_env g)
                        (elab_term st.pre)
                        vprop_tm &
          RT.tot_typing (elab_env g)
                        (mk_abs (elab_term st.res) R.Q_Explicit
                           (elab_term st.post))
                        (post1_type_bind (elab_term st.res)))
let stc_soundness
  (#g:stt_env)
  (#st:st_comp)
  (d_st:st_comp_typing g st)
  
  : GTot (RT.tot_typing (elab_env g)
                        (elab_term st.res)
                        (RT.tm_type st.u) &
          RT.tot_typing (elab_env g)
                        (elab_term st.pre)
                        vprop_tm &
          RT.tot_typing (elab_env g)
                        (mk_abs (elab_term st.res) R.Q_Explicit
                           (elab_term st.post))
                        (post1_type_bind (elab_term st.res))) =
   
  let STC _ st x dres dpre dpost = d_st in
  let res_typing = tot_typing_soundness dres in
  let pre_typing = tot_typing_soundness dpre in      
  calc (==) {
    RT.close_term (elab_term (open_term st.post x)) x;
       (==) { elab_open_commute st.post x }
    RT.close_term (RT.open_term (elab_term st.post) x) x;
       (==) { 
              elab_freevars st.post;
              RT.close_open_inverse (elab_term st.post) x
            }
    elab_term st.post;
  };
  let post_typing  = mk_t_abs_tot g ppname_default dres dpost in
  res_typing, pre_typing, post_typing
val stc_soundness
  (#g:stt_env)
  (#st:st_comp)
  (d_st:st_comp_typing g st)
  
  : GTot (RT.tot_typing ( elab_env g)
                        (elab_term st.res)
                        (RT.tm_type st.u) &
          RT.tot_typing (elab_env g)
                        (elab_term st.pre)
                        vprop_tm &
          RT.tot_typing (elab_env g)
                        (mk_abs (elab_term st.res) R.Q_Explicit
                           (elab_term st.post))
                        (post1_type_bind (elab_term st.res)))
let stc_soundness (#g: stt_env) (#st: st_comp) (d_st: st_comp_typing g st)
    : GTot
    (RT.tot_typing (elab_env g) (elab_term st.res) (RT.tm_type st.u) &
      RT.tot_typing (elab_env g) (elab_term st.pre) vprop_tm &
      RT.tot_typing (elab_env g)
        (mk_abs (elab_term st.res) R.Q_Explicit (elab_term st.post))
        (post1_type_bind (elab_term st.res))) =
let STC _ st x dres dpre dpost = d_st in
let res_typing = tot_typing_soundness dres in
let pre_typing = tot_typing_soundness dpre in
calc ( == ) {
  RT.close_term (elab_term (open_term st.post x)) x;
  ( == ) { elab_open_commute st.post x }
  RT.close_term (RT.open_term (elab_term st.post) x) x;
  ( == ) { (elab_freevars st.post;
    RT.close_open_inverse (elab_term st.post) x) }
  elab_term st.post;
};
let post_typing = mk_t_abs_tot g ppname_default dres dpost in
res_typing, pre_typing, post_typing
Pulse.Soundness.Comp.fst.checked
Pulse.Typing.fst.checked Pulse.Syntax.fst.checked Pulse.Soundness.STT.fsti.checked Pulse.Soundness.Common.fst.checked Pulse.Reflection.Util.fst.checked Pulse.Elaborate.Core.fst.checked Pulse.Elaborate.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Calc.fsti.checked
Pulse.Soundness.Comp.fst
Pulse.Soundness.Common.stt_env Pulse.Syntax.Base.st_comp Pulse.Typing.st_comp_typing Pulse.Typing.Env.env Pulse.Syntax.Base.var Prims.l_and Prims.b2t FStar.Pervasives.Native.uu___is_None Pulse.Syntax.Base.typ Pulse.Typing.Env.lookup Prims.l_not FStar.Set.mem Pulse.Syntax.Naming.freevars Pulse.Syntax.Base.__proj__Mkst_comp__item__post Pulse.Typing.universe_of Pulse.Syntax.Base.__proj__Mkst_comp__item__res Pulse.Syntax.Base.__proj__Mkst_comp__item__u Pulse.Typing.tot_typing Pulse.Syntax.Base.__proj__Mkst_comp__item__pre Pulse.Syntax.Base.tm_vprop Pulse.Typing.Env.push_binding Pulse.Syntax.Base.ppname_default Pulse.Syntax.Naming.open_term FStar.Pervasives.Native.Mktuple3 FStar.Reflection.Typing.tot_typing Pulse.Typing.elab_env Pulse.Elaborate.Pure.elab_term FStar.Reflection.Typing.tm_type Pulse.Reflection.Util.vprop_tm Pulse.Reflection.Util.mk_abs FStar.Reflection.V2.Data.Q_Explicit Pulse.Soundness.Common.post1_type_bind Pulse.Reflection.Util.mk_abs_with_name Pulse.Syntax.Base.__proj__Mkppname__item__name Pulse.Elaborate.Pure.elab_qual FStar.Pervasives.Native.None Pulse.Syntax.Base.qualifier Pulse.Syntax.Pure.tm_arrow Pulse.Syntax.Base.Mkbinder Pulse.Syntax.Naming.close_comp Pulse.Syntax.Base.C_Tot Pulse.Soundness.Common.mk_t_abs_tot Prims.unit FStar.Calc.calc_finish FStar.Reflection.Types.term Prims.eq2 FStar.Reflection.Typing.close_term Prims.Cons FStar.Preorder.relation Prims.Nil FStar.Calc.calc_step FStar.Reflection.Typing.open_term FStar.Calc.calc_init FStar.Calc.calc_pack Pulse.Elaborate.elab_open_commute Prims.squash FStar.Reflection.Typing.close_open_inverse Pulse.Elaborate.elab_freevars Pulse.Soundness.Common.tot_typing_soundness Pulse.Syntax.Pure.tm_type FStar.Pervasives.Native.tuple3
module Pulse.Soundness.Comp

open Pulse.Syntax
open Pulse.Reflection.Util
open Pulse.Typing
open Pulse.Elaborate.Core
open Pulse.Elaborate
open Pulse.Soundness.Common

module STT = Pulse.Soundness.STT

let stc_soundness
  (#g:stt_env)
  (#st:st_comp)
  (d_st:st_comp_typing g st)
  
  : GTot (RT.tot_typing (elab_env g)
                        (elab_term st.res)
                        (RT.tm_type st.u) &
          RT.tot_typing (elab_env g)
                        (elab_term st.pre)
                        vprop_tm &
          RT.tot_typing (elab_env g)
                        (mk_abs (elab_term st.res) R.Q_Explicit
val stc_soundness
  (#g:stt_env)
  (#st:st_comp)
  (d_st:st_comp_typing g st)
  
  : GTot (RT.tot_typing ( elab_env g)
                        (elab_term st.res)
                        (RT.tm_type st.u) &
          RT.tot_typing (elab_env g)
                        (elab_term st.pre)
                        vprop_tm &
          RT.tot_typing (elab_env g)
                        (mk_abs (elab_term st.res) R.Q_Explicit
                           (elab_term st.post))
                        (post1_type_bind (elab_term st.res)))
d_st: Pulse.Typing.st_comp_typing g st
  -> Prims.GTot
    ((FStar.Reflection.Typing.tot_typing (Pulse.Typing.elab_env g)
        (Pulse.Elaborate.Pure.elab_term (Mkst_comp?.res st))
        (FStar.Reflection.Typing.tm_type (Mkst_comp?.u st)) *
      FStar.Reflection.Typing.tot_typing (Pulse.Typing.elab_env g)
        (Pulse.Elaborate.Pure.elab_term (Mkst_comp?.pre st))
        Pulse.Reflection.Util.vprop_tm) *
      FStar.Reflection.Typing.tot_typing (Pulse.Typing.elab_env g)
        (Pulse.Reflection.Util.mk_abs (Pulse.Elaborate.Pure.elab_term (Mkst_comp?.res st))
            FStar.Reflection.V2.Data.Q_Explicit
            (Pulse.Elaborate.Pure.elab_term (Mkst_comp?.post st)))
        (Pulse.Soundness.Common.post1_type_bind (Pulse.Elaborate.Pure.elab_term (Mkst_comp?.res st))
        ))