val withlocal_soundness
  (#g:stt_env)
  (#t:st_term)
  (#c:comp)
  (d:st_typing g t c{T_WithLocal? d})
  (soundness:soundness_t d)
  : GTot (RT.tot_typing (elab_env g)
                        (elab_st_typing d)
                        (elab_comp c))
let withlocal_soundness #g #t #c d soundness =
  let T_WithLocal _ init body init_t c x init_typing init_t_typing c_typing body_typing = d in
  let CT_ST _ st st_typing = c_typing in
  
  let rg =  elab_env g in
  let ru = comp_u c in
  let ra = elab_term init_t in
  let rinit = elab_term init in
  let rpre = elab_term (comp_pre c) in
  let rret_t = elab_term (comp_res c) in
  let rpost = elab_term (comp_post c) in
  let rbody = elab_st_typing body_typing in

  let a_typing = tot_typing_soundness init_t_typing in
  let rinit_typing = tot_typing_soundness init_typing in
  let cres_typing, cpre_typing, cpost_typing =
    Pulse.Soundness.Comp.stc_soundness st_typing in

  let pre_typing = cpre_typing in
  let ret_t_typing = cres_typing in
  let post_typing = cpost_typing in

  elab_push_binding g x (mk_array init_t);
  let rbody_typing = soundness _ _ _ body_typing in

  WT.with_local_typing
    #rg
    #ru
    #ra
    #rinit
    #rpre
    #rret_t
    #rpost
    #rbody
    x
    a_typing
    rinit_typing
    pre_typing
    ret_t_typing
    post_typing
    rbody_typing
val withlocal_soundness
  (#g:stt_env)
  (#t:st_term)
  (#c:comp)
  (d:st_typing g t c{T_WithLocal? d})
  (soundness:soundness_t d)
  : GTot (RT.tot_typing (elab_env g)
                        (elab_st_typing d)
                        (elab_comp c))
let withlocal_soundness #g #t #c d soundness =
let T_WithLocal _ init body init_t c x init_typing init_t_typing c_typing body_typing = d in
let CT_ST _ st st_typing = c_typing in
let rg = elab_env g in
let ru = comp_u c in
let ra = elab_term init_t in
let rinit = elab_term init in
let rpre = elab_term (comp_pre c) in
let rret_t = elab_term (comp_res c) in
let rpost = elab_term (comp_post c) in
let rbody = elab_st_typing body_typing in
let a_typing = tot_typing_soundness init_t_typing in
let rinit_typing = tot_typing_soundness init_typing in
let cres_typing, cpre_typing, cpost_typing = Pulse.Soundness.Comp.stc_soundness st_typing in
let pre_typing = cpre_typing in
let ret_t_typing = cres_typing in
let post_typing = cpost_typing in
elab_push_binding g x (mk_array init_t);
let rbody_typing = soundness _ _ _ body_typing in
WT.with_local_typing #rg #ru #ra #rinit #rpre #rret_t #rpost #rbody x a_typing rinit_typing
  pre_typing ret_t_typing post_typing rbody_typing
Pulse.Soundness.WithLocal.fst.checked
Pulse.Typing.fst.checked Pulse.Syntax.fst.checked Pulse.Steel.Wrapper.Typing.fsti.checked Pulse.Soundness.Comp.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.fsti.checked
Pulse.Soundness.WithLocal.fst
Pulse.Soundness.Common.stt_env Pulse.Syntax.Base.st_term Pulse.Syntax.Base.comp Pulse.Typing.st_typing Prims.b2t Pulse.Typing.uu___is_T_WithLocal Pulse.Soundness.Common.soundness_t Pulse.Typing.Env.env Pulse.Syntax.Base.term Pulse.Syntax.Base.uu___is_C_ST Pulse.Syntax.Base.var Prims.l_and FStar.Pervasives.Native.uu___is_None Pulse.Syntax.Base.typ Pulse.Typing.Env.lookup Prims.l_not FStar.Set.mem Pulse.Syntax.Naming.freevars_st Pulse.Typing.tot_typing Pulse.Typing.universe_of Pulse.Syntax.Pure.u0 Pulse.Typing.comp_typing Pulse.Syntax.Base.comp_u Pulse.Typing.Env.push_binding Pulse.Syntax.Base.ppname_default Pulse.Typing.mk_ref Pulse.Syntax.Naming.open_st_term_nv Pulse.Syntax.Base.v_as_nv Pulse.Typing.comp_withlocal_body Pulse.Syntax.Base.st_comp Pulse.Typing.st_comp_typing FStar.Reflection.Typing.tot_typing Pulse.Typing.elab_env Pulse.Elaborate.Pure.elab_term Pulse.Syntax.Base.__proj__Mkst_comp__item__res FStar.Reflection.Typing.tm_type Pulse.Syntax.Base.__proj__Mkst_comp__item__u Pulse.Syntax.Base.__proj__Mkst_comp__item__pre Pulse.Reflection.Util.vprop_tm Pulse.Reflection.Util.mk_abs FStar.Reflection.V2.Data.Q_Explicit Pulse.Syntax.Base.__proj__Mkst_comp__item__post Pulse.Soundness.Common.post1_type_bind Pulse.Steel.Wrapper.Typing.with_local_typing Pulse.Elaborate.Core.elab_st_typing Pulse.Elaborate.Pure.elab_comp Prims.unit Pulse.Typing.elab_push_binding Pulse.Typing.mk_array FStar.Pervasives.Native.tuple3 Pulse.Soundness.Comp.stc_soundness Pulse.Soundness.Common.tot_typing_soundness Pulse.Syntax.Pure.tm_type FStar.Reflection.Types.term Pulse.Syntax.Base.comp_post Pulse.Syntax.Base.comp_res Pulse.Syntax.Base.comp_pre Pulse.Syntax.Base.universe FStar.Reflection.Types.env
module Pulse.Soundness.WithLocal

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

module WT = Pulse.Steel.Wrapper.Typing
val withlocal_soundness
  (#g:stt_env)
  (#t:st_term)
  (#c:comp)
  (d:st_typing g t c{T_WithLocal? d})
  (soundness:soundness_t d)
  : GTot (RT.tot_typing (elab_env g)
                        (elab_st_typing d)
                        (elab_comp c))
d: Pulse.Typing.st_typing g t c {T_WithLocal? d} -> soundness: Pulse.Soundness.Common.soundness_t d
  -> Prims.GTot
    (FStar.Reflection.Typing.tot_typing (Pulse.Typing.elab_env g)
        (Pulse.Elaborate.Core.elab_st_typing d)
        (Pulse.Elaborate.Pure.elab_comp c))