val st_typing_correctness (#g:env) (#t:st_term) (#c:comp_st) 
                          (_:st_typing g t c)
  : comp_typing_u g c
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
val st_typing_correctness (#g:env) (#t:st_term) (#c:comp_st) 
                          (_:st_typing g t c)
  : comp_typing_u g c
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
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_term Pulse.Syntax.Base.comp_st Pulse.Typing.st_typing Pulse.Typing.Metatheory.Base.admit_comp_typing Pulse.Typing.Metatheory.Base.comp_typing_u
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)
val st_typing_correctness (#g:env) (#t:st_term) (#c:comp_st) 
                          (_:st_typing g t c)
  : comp_typing_u g c
_: Pulse.Typing.st_typing g t c -> Pulse.Typing.Metatheory.Base.comp_typing_u g c