val 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)]
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 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)]
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
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.Reflection.Types.env Pulse.Typing.Env.env_bindings FStar.Reflection.Types.fv FStar.Reflection.V2.Data.universes Pulse.Typing.Env.binding Prims.list Pulse.Soundness.Common.extend_env_l_lookup_fvar Prims.unit Prims.l_True Prims.squash Prims.eq2 FStar.Pervasives.Native.option FStar.Reflection.Types.term FStar.Reflection.Typing.lookup_fvar_uinst Pulse.Typing.extend_env_l Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.Nil
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)
val 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)]

    g: FStar.Reflection.Types.env ->
    sg: Pulse.Typing.Env.env_bindings ->
    fv: FStar.Reflection.Types.fv ->
    us: FStar.Reflection.V2.Data.universes
  -> FStar.Pervasives.Lemma
      (ensures
        FStar.Reflection.Typing.lookup_fvar_uinst (Pulse.Typing.extend_env_l g sg) fv us ==
        FStar.Reflection.Typing.lookup_fvar_uinst g fv us)
      [SMTPat (FStar.Reflection.Typing.lookup_fvar_uinst (Pulse.Typing.extend_env_l g sg) fv us)]