let elab_term_opt (b:option term) =
  match b with
  | Some b -> Some (elab_term b)
  | None -> None
let elab_term_opt (b: option term) =
match b with
| Some b -> Some (elab_term b)
| None -> None
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
FStar.Pervasives.Native.option Pulse.Syntax.Base.term FStar.Pervasives.Native.Some FStar.Reflection.Types.term Pulse.Elaborate.Pure.elab_term FStar.Pervasives.Native.None
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
val elab_term_opt : b: FStar.Pervasives.Native.option Pulse.Syntax.Base.term
  -> FStar.Pervasives.Native.option FStar.Reflection.Types.term
b: FStar.Pervasives.Native.option Pulse.Syntax.Base.term
  -> FStar.Pervasives.Native.option FStar.Reflection.Types.term