val non_informative_c_weakening
      (g g': env)
      (g1: env{pairwise_disjoint g g1 g'})
      (c: comp_st)
      (d: non_informative_c (push_env g g') c)
    : non_informative_c (push_env (push_env g g1) g') c
let non_informative_c_weakening (g g':env) (g1:env{ pairwise_disjoint g g1 g' })
  (c:comp_st)
  (d:non_informative_c (push_env g g') c)
  : non_informative_c (push_env (push_env g g1) g') c =
  non_informative_t_weakening g g' g1 _ _ d
val non_informative_c_weakening
      (g g': env)
      (g1: env{pairwise_disjoint g g1 g'})
      (c: comp_st)
      (d: non_informative_c (push_env g g') c)
    : non_informative_c (push_env (push_env g g1) g') c
let non_informative_c_weakening
      (g g': env)
      (g1: env{pairwise_disjoint g g1 g'})
      (c: comp_st)
      (d: non_informative_c (push_env g g') c)
    : non_informative_c (push_env (push_env g g1) g') c =
non_informative_t_weakening g g' g1 _ _ d
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.Typing.Env.pairwise_disjoint Pulse.Syntax.Base.comp_st Pulse.Typing.non_informative_c Pulse.Typing.Env.push_env Pulse.Typing.Metatheory.Base.non_informative_t_weakening Pulse.Syntax.Base.comp_u Pulse.Syntax.Base.comp_res
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())

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

let tm_exists_inversion (#g:env) (#u:universe) (#ty:term) (#p:term) 
                        (_:tot_typing g (tm_exists_sl u (as_binder ty) p) tm_vprop)
                        (x:var { fresh_wrt x g (freevars p) } )
  : universe_of g ty u &
    tot_typing (push_binding g x ppname_default ty) p tm_vprop
  = admit(), admit()

let pure_typing_inversion (#g:env) (#p:term) (_:tot_typing g (tm_pure p) tm_vprop)
   : tot_typing g p (tm_fstar FStar.Reflection.Typing.tm_prop Range.range_0)
   = admit ()

let tot_typing_weakening _ _ _ _ _ _ = admit ()

let non_informative_t_weakening (g g':env) (g1:env{ pairwise_disjoint g g1 g' })
  (u:universe) (t:term)
  (d:non_informative_t (push_env g g') u t)
  : non_informative_t (push_env (push_env g g1) g') u t =
  let (| w, _ |) = d in
  (| w, magic () |)

let non_informative_c_weakening (g g':env) (g1:env{ pairwise_disjoint g g1 g' })
  (c:comp_st)
  (d:non_informative_c (push_env g g') c)
val non_informative_c_weakening
      (g g': env)
      (g1: env{pairwise_disjoint g g1 g'})
      (c: comp_st)
      (d: non_informative_c (push_env g g') c)
    : non_informative_c (push_env (push_env g g1) g') c

    g: Pulse.Typing.Env.env ->
    g': Pulse.Typing.Env.env ->
    g1: Pulse.Typing.Env.env{Pulse.Typing.Env.pairwise_disjoint g g1 g'} ->
    c: Pulse.Syntax.Base.comp_st ->
    d: Pulse.Typing.non_informative_c (Pulse.Typing.Env.push_env g g') c
  -> Pulse.Typing.non_informative_c (Pulse.Typing.Env.push_env (Pulse.Typing.Env.push_env g g1) g')
      c