let abs_and_app0 (ty:R.term) (b:R.term) =
    R.mk_app (mk_abs ty R.Q_Explicit b) [bound_var 0, R.Q_Explicit]
let abs_and_app0 (ty b: R.term) =
R.mk_app (mk_abs ty R.Q_Explicit b) [bound_var 0, R.Q_Explicit]
Pulse.Soundness.STEquiv.fst.checked
Pulse.Typing.Combinators.fsti.checked Pulse.Typing.fst.checked Pulse.Syntax.fst.checked Pulse.Soundness.VPropEquiv.fsti.checked Pulse.Soundness.Common.fst.checked Pulse.Reflection.Util.fst.checked Pulse.Elaborate.Pure.fst.checked Pulse.Elaborate.fsti.checked Pulse.Checker.VPropEquiv.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.STEquiv.fst
FStar.Reflection.Types.term FStar.Reflection.V2.Derived.mk_app Pulse.Reflection.Util.mk_abs FStar.Reflection.V2.Data.Q_Explicit Prims.Cons FStar.Reflection.V2.Data.argv FStar.Pervasives.Native.Mktuple2 FStar.Reflection.V2.Data.aqualv Pulse.Reflection.Util.bound_var Prims.Nil
module Pulse.Soundness.STEquiv
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.Elaborate.Pure
open Pulse.Typing
open Pulse.Typing.Combinators
open Pulse.Elaborate
open Pulse.Soundness.Common
open Pulse.Checker.VPropEquiv


let stt_vprop_equiv_closing (t0 t1:R.term) (x:var)
  : Lemma (RT.close_term (stt_vprop_equiv t0 t1) x ==
           stt_vprop_equiv (RT.close_term t0 x) (RT.close_term t1 x))
           [SMTPat (RT.close_term (stt_vprop_equiv t0 t1) x)]
  = RT.close_term_spec (stt_vprop_equiv t0 t1) x;
    RT.close_term_spec t0 x;
    RT.close_term_spec t1 x

let app0 t = R.mk_app t [bound_var 0, R.Q_Explicit]
val abs_and_app0 : ty: FStar.Reflection.Types.term -> b: FStar.Reflection.Types.term -> FStar.Reflection.Types.term
ty: FStar.Reflection.Types.term -> b: FStar.Reflection.Types.term -> FStar.Reflection.Types.term