val vprop_equiv_typing_fwd
      (#g: env)
      (#ctxt: _)
      (ctxt_typing: tot_typing g ctxt tm_vprop)
      (#p: _)
      (d: vprop_equiv g ctxt p)
    : tot_typing g p tm_vprop
let vprop_equiv_typing_fwd (#g:env) (#ctxt:_) (ctxt_typing:tot_typing g ctxt tm_vprop)
                           (#p:_) (d:vprop_equiv g ctxt p)
  : tot_typing g p tm_vprop 
  = let fwd, _ = vprop_equiv_typing d in
    fwd ctxt_typing
val vprop_equiv_typing_fwd
      (#g: env)
      (#ctxt: _)
      (ctxt_typing: tot_typing g ctxt tm_vprop)
      (#p: _)
      (d: vprop_equiv g ctxt p)
    : tot_typing g p tm_vprop
let vprop_equiv_typing_fwd
      (#g: env)
      (#ctxt: _)
      (ctxt_typing: tot_typing g ctxt tm_vprop)
      (#p: _)
      (d: vprop_equiv g ctxt p)
    : tot_typing g p tm_vprop =
let fwd, _ = vprop_equiv_typing d in
fwd ctxt_typing
Pulse.Checker.VPropEquiv.fsti.checked
Pulse.Typing.Combinators.fsti.checked Pulse.Typing.fst.checked Pulse.Syntax.fst.checked Pulse.Checker.Base.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Pulse.Checker.VPropEquiv.fsti
Pulse.Typing.Env.env Pulse.Syntax.Base.term Pulse.Typing.tot_typing Pulse.Syntax.Base.tm_vprop Pulse.Typing.vprop_equiv FStar.Pervasives.Native.tuple2 Pulse.Typing.Combinators.vprop_equiv_typing
module Pulse.Checker.VPropEquiv

open FStar.List.Tot

open Pulse.Syntax
open Pulse.Typing
open Pulse.Typing.Combinators

open Pulse.Checker.Base

let canon_vprop (vp:term)
  : term
  = list_as_vprop (vprop_as_list vp)


val ve_unit_r (g:env) (p:term) : vprop_equiv g (tm_star p tm_emp) p

val list_as_vprop_append (g:env) (vp0 vp1:list term)
  : GTot (vprop_equiv g (list_as_vprop (vp0 @ vp1))
                        (tm_star (list_as_vprop vp0) 
                                 (list_as_vprop vp1)))

val list_as_vprop_comm (g:env) (vp0 vp1:list term)
  : GTot (vprop_equiv g (list_as_vprop (vp0 @ vp1))
                        (list_as_vprop (vp1 @ vp0)))

val list_as_vprop_assoc (g:env) (vp0 vp1 vp2:list term)
  : GTot (vprop_equiv g (list_as_vprop (vp0 @ (vp1 @ vp2)))
                        (list_as_vprop ((vp0 @ vp1) @ vp2)))

val list_as_vprop_ctx (g:env) (vp0 vp0' vp1 vp1':list term)
                      (_:vprop_equiv g (list_as_vprop vp0) (list_as_vprop vp0'))
                      (_:vprop_equiv g (list_as_vprop vp1) (list_as_vprop vp1'))
  : GTot (vprop_equiv g (list_as_vprop (vp0 @ vp1)) (list_as_vprop (vp0' @ vp1')))

val list_as_vprop_singleton (g:env) (p q:term) (d:vprop_equiv g p q)
  : GTot (vprop_equiv g (list_as_vprop [p]) (list_as_vprop [q]))
  
val vprop_list_equiv (g:env)  (vp:term)
  : GTot (vprop_equiv g vp (canon_vprop vp))

val vprop_equiv_swap_equiv (g:_) (l0 l2:list term)
                           (p q:term) (d_p_q:vprop_equiv g p q)
  : GTot (vprop_equiv g (list_as_vprop ((l0 @ [q]) @ l2))
                        (list_as_vprop ([p] @ (l0 @ l2))))

val vprop_equiv_split_frame (g:_) (ctxt req:term) (frame:list term)
                            (d:vprop_equiv g (list_as_vprop (vprop_as_list req @ frame))
                                             (list_as_vprop (vprop_as_list ctxt)))
  : vprop_equiv g (tm_star req (list_as_vprop frame)) ctxt


let vprop_equiv_typing_fwd (#g:env) (#ctxt:_) (ctxt_typing:tot_typing g ctxt tm_vprop)
                           (#p:_) (d:vprop_equiv g ctxt p)
val vprop_equiv_typing_fwd
      (#g: env)
      (#ctxt: _)
      (ctxt_typing: tot_typing g ctxt tm_vprop)
      (#p: _)
      (d: vprop_equiv g ctxt p)
    : tot_typing g p tm_vprop

    ctxt_typing: Pulse.Typing.tot_typing g ctxt Pulse.Syntax.Base.tm_vprop ->
    d: Pulse.Typing.vprop_equiv g ctxt p
  -> Pulse.Typing.tot_typing g p Pulse.Syntax.Base.tm_vprop