val st_comp_typing_inversion (#g:env) (#st:_) (ct:st_comp_typing g st)
  : (universe_of g st.res st.u &
     tot_typing g st.pre tm_vprop &
     x:var{fresh_wrt x g (freevars st.post)} &
     tot_typing (push_binding g x ppname_default st.res) (open_term st.post x) tm_vprop)
let st_comp_typing_inversion (#g:env) (#st:_) (ct:st_comp_typing g st) = 
  let STC g st x ty pre post = ct in
  (| ty, pre, x, post |)
val st_comp_typing_inversion (#g:env) (#st:_) (ct:st_comp_typing g st)
  : (universe_of g st.res st.u &
     tot_typing g st.pre tm_vprop &
     x:var{fresh_wrt x g (freevars st.post)} &
     tot_typing (push_binding g x ppname_default st.res) (open_term st.post x) tm_vprop)
let st_comp_typing_inversion (#g: env) (#st: _) (ct: st_comp_typing g st) =
let STC g st x ty pre post = ct in
(| ty, pre, x, post |)
Pulse.Typing.Metatheory.Base.fst.checked
Pulse.Typing.fst.checked Pulse.Syntax.Naming.fsti.checked Pulse.Syntax.fst.checked prims.fst.checked FStar.Set.fsti.checked FStar.Reflection.Typing.fsti.checked FStar.Range.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Pulse.Typing.Metatheory.Base.fst
Pulse.Typing.Env.env Pulse.Syntax.Base.st_comp Pulse.Typing.st_comp_typing 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.Mkdtuple4 Pulse.Typing.fresh_wrt FStar.Pervasives.dtuple4
module Pulse.Typing.Metatheory.Base
open Pulse.Syntax
open Pulse.Syntax.Naming
open Pulse.Typing

module RT = FStar.Reflection.Typing

let admit_st_comp_typing (g:env) (st:st_comp) 
  : st_comp_typing g st
  = admit(); 
    STC g st (fresh g) (admit()) (admit()) (admit())

let admit_comp_typing (g:env) (c:comp_st)
  : comp_typing_u g c
  = match c with
    | C_ST st ->
      CT_ST g st (admit_st_comp_typing g st)
    | C_STAtomic inames st ->
      CT_STAtomic g inames st (admit()) (admit_st_comp_typing g st)
    | C_STGhost inames st ->
      CT_STGhost g inames st (admit()) (admit_st_comp_typing g st)      

let st_typing_correctness (#g:env) (#t:st_term) (#c:comp_st) 
                          (_:st_typing g t c)
  : comp_typing_u g c
  = admit_comp_typing g c
    
let add_frame_well_typed (#g:env) (#c:comp_st) (ct:comp_typing_u g c)
                         (#f:term) (ft:tot_typing g f tm_vprop)
  : comp_typing_u g (add_frame c f)
  = admit_comp_typing _ _

let comp_typing_inversion #g #c ct = 
  match ct with
  | CT_ST _ _ st
  | CT_STAtomic _ _ _ _ st 
  | CT_STGhost _ _ _ _ st   -> st

let st_comp_typing_inversion_cofinite (#g:env) (#st:_) (ct:st_comp_typing g st) = 
  admit(), admit(), (fun _ -> admit())
val st_comp_typing_inversion (#g:env) (#st:_) (ct:st_comp_typing g st)
  : (universe_of g st.res st.u &
     tot_typing g st.pre tm_vprop &
     x:var{fresh_wrt x g (freevars st.post)} &
     tot_typing (push_binding g x ppname_default st.res) (open_term st.post x) tm_vprop)
ct: Pulse.Typing.st_comp_typing g st
  -> FStar.Pervasives.dtuple4 (Pulse.Typing.universe_of g (Mkst_comp?.res st) (Mkst_comp?.u st))
      (fun _ -> Pulse.Typing.tot_typing g (Mkst_comp?.pre st) Pulse.Syntax.Base.tm_vprop)
      (fun _ _ ->
          x:
          Pulse.Syntax.Base.var
            {Pulse.Typing.fresh_wrt x g (Pulse.Syntax.Naming.freevars (Mkst_comp?.post st))})
      (fun _ _ x ->
          Pulse.Typing.tot_typing (Pulse.Typing.Env.push_binding g
                x
                Pulse.Syntax.Base.ppname_default
                (Mkst_comp?.res st))
            (Pulse.Syntax.Naming.open_term (Mkst_comp?.post st) x)
            Pulse.Syntax.Base.tm_vprop)