val ghost_typing_soundness (#g: env) (#e #t: term) (d: ghost_typing g e t)
    : GTot (RT.ghost_typing (elab_env g) (elab_term e) (elab_term t))
let ghost_typing_soundness (#g:env)
                           (#e:term)
                           (#t:term)
                           (d:ghost_typing g e t)
  : GTot (RT.ghost_typing (elab_env g) (elab_term e) (elab_term t))
  = let E d = d in
    d
val ghost_typing_soundness (#g: env) (#e #t: term) (d: ghost_typing g e t)
    : GTot (RT.ghost_typing (elab_env g) (elab_term e) (elab_term t))
let ghost_typing_soundness (#g: env) (#e #t: term) (d: ghost_typing g e t)
    : GTot (RT.ghost_typing (elab_env g) (elab_term e) (elab_term t)) =
let E d = d in
d
Pulse.Soundness.Common.fst.checked
Pulse.Typing.fst.checked Pulse.Syntax.fst.checked Pulse.Reflection.Util.fst.checked Pulse.Elaborate.fsti.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Set.fsti.checked FStar.Reflection.V2.fst.checked FStar.Reflection.Typing.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Pulse.Soundness.Common.fst
Pulse.Typing.Env.env Pulse.Syntax.Base.term Pulse.Typing.ghost_typing FStar.Reflection.Typing.typing Pulse.Typing.elab_env Pulse.Elaborate.Pure.elab_term FStar.Pervasives.Native.Mktuple2 FStar.Stubs.TypeChecker.Core.tot_or_ghost FStar.Reflection.Types.typ FStar.Stubs.TypeChecker.Core.E_Ghost FStar.Reflection.Typing.ghost_typing
module Pulse.Soundness.Common
module RT = FStar.Reflection.Typing
module R = FStar.Reflection.V2
module L = FStar.List.Tot
module T = FStar.Tactics.V2
open FStar.List.Tot
open Pulse.Syntax
open Pulse.Reflection.Util
open Pulse.Typing
open Pulse.Elaborate

let ln_comp = c:comp_st { ln_c c }

let rec extend_env_l_lookup_fvar (g:R.env) (sg:env_bindings) (fv:R.fv) (us:R.universes)
  : Lemma 
    (ensures
      RT.lookup_fvar_uinst (extend_env_l g sg) fv us ==
      RT.lookup_fvar_uinst g fv us)
    [SMTPat (RT.lookup_fvar_uinst (extend_env_l g sg) fv us)]
  = match sg with
    | [] -> ()
    | hd::tl -> extend_env_l_lookup_fvar g tl fv us


let elab_term_opt (b:option term) =
  match b with
  | Some b -> Some (elab_term b)
  | None -> None

// let rec extend_env_l_lookup_bvar (g:R.env) (sg:env_bindings) (x:var)
//   : Lemma 
//     (requires (forall x. RT.lookup_bvar g x == None))
//     (ensures (RT.lookup_bvar (extend_env_l g sg) x == elab_term_opt (lookup sg x)))
//     (decreases sg)
//     [SMTPat (RT.lookup_bvar (extend_env_l g sg) x)]
//   = match sg with
//     | [] -> ()
//     | hd :: tl -> extend_env_l_lookup_bvar g tl x

let lookup_elab_env (g:env) (x:var)
  : Lemma 
    (ensures (RT.lookup_bvar (elab_env g) x == elab_term_opt (lookup g x)))
    [SMTPat (RT.lookup_bvar (elab_env g) x)]
  = admit ()  // TODO: FIX ME!!!!
  
let tot_typing_soundness (#g:env)
                         (#e:term)
                         (#t:term)
                         (d:tot_typing g e t)
  : GTot (RT.tot_typing (elab_env g) (elab_term e) (elab_term t))
  = let E d = d in
    d

let ghost_typing_soundness (#g:env)
                           (#e:term)
                           (#t:term)
                           (d:ghost_typing g e t)
val ghost_typing_soundness (#g: env) (#e #t: term) (d: ghost_typing g e t)
    : GTot (RT.ghost_typing (elab_env g) (elab_term e) (elab_term t))
d: Pulse.Typing.ghost_typing g e t
  -> Prims.GTot
    (FStar.Reflection.Typing.ghost_typing (Pulse.Typing.elab_env g)
        (Pulse.Elaborate.Pure.elab_term e)
        (Pulse.Elaborate.Pure.elab_term t))