val vprop_arrow (t: term) : term
let vprop_arrow (t:term) : term = tm_arrow (null_binder t) None (C_Tot tm_vprop)
val vprop_arrow (t: term) : term
let vprop_arrow (t: term) : term =
tm_arrow (null_binder t) None (C_Tot tm_vprop)
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
Pulse.Syntax.Base.term Pulse.Syntax.Pure.tm_arrow Pulse.Syntax.Base.null_binder FStar.Pervasives.Native.None Pulse.Syntax.Base.qualifier Pulse.Syntax.Base.C_Tot Pulse.Syntax.Base.tm_vprop
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]

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]


// x:ty -> vprop_equiv p q ~ x:ty -> vprop_equiv ((fun y -> p) x) ((fun y -> q) x)
let stt_vprop_equiv_abstract (#g:stt_env) (#post0 #post1:term) (#pf:_) (#ty:_)
                             (d:RT.tot_typing (elab_env g) pf 
                                  (mk_arrow (ty, R.Q_Explicit)
                                     (stt_vprop_equiv (elab_term post0) (elab_term post1))))
  : GTot (RT.tot_typing (elab_env g) pf
            (mk_arrow (ty, R.Q_Explicit)
                      (stt_vprop_equiv (abs_and_app0 ty (elab_term post0))
                                       (abs_and_app0 ty (elab_term post1)))))
  = admit()

let inst_intro_vprop_post_equiv (#g:R.env) (#ty:R.term) (#u:_)
                                (d_ty:RT.tot_typing g ty (RT.tm_type u))
                                (#post0 #post1:R.term)
                                (d_0:RT.tot_typing g post0 
                                       (mk_arrow (ty, R.Q_Explicit) (elab_term tm_vprop)))
                                (d_1:RT.tot_typing g post1 
                                       (mk_arrow (ty, R.Q_Explicit) (elab_term tm_vprop)))
                                (#pf:_)
                                (eq:RT.tot_typing g pf (mk_arrow (ty, R.Q_Explicit) 
                                      (stt_vprop_equiv (app0 post0) (app0 post1))))
  : GTot ( pf: R.term &
           RT.tot_typing g pf (stt_vprop_post_equiv u ty post0 post1) )
  = admit()


let stt_vprop_post_equiv_is_prop (#g:R.env) (#ty:R.term) (#u:_)
                                 (d_ty:RT.tot_typing g ty (RT.tm_type u))
                                 (#post0 #post1:R.term)
                                 (d_0:RT.tot_typing g post0 
                                                (mk_arrow (ty, R.Q_Explicit) (elab_term tm_vprop)))
                                 (d_1:RT.tot_typing g post1 
                                                (mk_arrow (ty, R.Q_Explicit) (elab_term tm_vprop)))
  : GTot (RT.tot_typing g (stt_vprop_post_equiv u ty post0 post1) RT.tm_prop)
  = admit()

let inst_sub_stt (#g:R.env) (#u:_) (#a #pre1 #pre2 #post1 #post2 #r:R.term)
                 (d_a: RT.tot_typing g a (RT.tm_type u))
                 (d_pre1: RT.tot_typing g pre1 (elab_term tm_vprop))
                 (d_pre2: RT.tot_typing g pre2 (elab_term tm_vprop))
                 (d_post1:RT.tot_typing g post1 (mk_arrow (a, R.Q_Explicit) (elab_term tm_vprop)))
                 (d_post2:RT.tot_typing g post2 (mk_arrow (a, R.Q_Explicit) (elab_term tm_vprop)))
                 (pre_equiv:RT.tot_typing g (`()) (stt_vprop_equiv pre1 pre2))
                 (post_equiv:RT.tot_typing g (`()) (stt_vprop_post_equiv u a post1 post2))
                 (d_r:RT.tot_typing g r (mk_stt_comp u a pre1 post1))
  : GTot (RT.tot_typing g (mk_sub_stt u a pre1 pre2 post1 post2 r) (mk_stt_comp u a pre2 post2))
  = admit()
val vprop_arrow (t: term) : term
t: Pulse.Syntax.Base.term -> Pulse.Syntax.Base.term