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]))
let list_as_vprop_singleton g
  (p q:term)
  (d:vprop_equiv g p q)
  : GTot (vprop_equiv g (list_as_vprop [p]) (list_as_vprop [q]))
  = VE_Ctxt _ p tm_emp q tm_emp d (VE_Refl _ tm_emp)
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]))
let list_as_vprop_singleton g (p: term) (q: term) (d: vprop_equiv g p q)
    : GTot (vprop_equiv g (list_as_vprop [p]) (list_as_vprop [q])) =
VE_Ctxt _ p tm_emp q tm_emp d (VE_Refl _ tm_emp)
Pulse.Checker.VPropEquiv.fst.checked
Pulse.Typing.fst.checked Pulse.Syntax.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Pulse.Checker.VPropEquiv.fst
Pulse.Typing.Env.env Pulse.Syntax.Base.term Pulse.Typing.vprop_equiv Pulse.Typing.VE_Ctxt Pulse.Syntax.Base.tm_emp Pulse.Typing.VE_Refl Pulse.Typing.Combinators.list_as_vprop Prims.Cons Prims.Nil
module Pulse.Checker.VPropEquiv
open Pulse.Syntax
open Pulse.Typing
open FStar.List.Tot

let ve_unit_r g (p:term) : vprop_equiv g (tm_star p tm_emp) p = 
  VE_Trans _ _ _ _ (VE_Comm _ _ _) (VE_Unit _ _)
      
let rec list_as_vprop_append g (vp0 vp1:list term)
  : GTot (vprop_equiv g (list_as_vprop (vp0 @ vp1))
                        (tm_star (list_as_vprop vp0) 
                                 (list_as_vprop vp1)))
         (decreases vp0)
  = match vp0 with
    | [] -> 
      let v : vprop_equiv g (list_as_vprop vp1)
                            (tm_star tm_emp (list_as_vprop vp1)) = VE_Sym _ _ _ (VE_Unit _ _)
      in
      v
    | hd::tl ->
      let tl_vp1 = list_as_vprop_append g tl vp1 in
      let d : vprop_equiv g (list_as_vprop (vp0 @ vp1))
                              (tm_star hd (tm_star (list_as_vprop tl) (list_as_vprop vp1)))
            = VE_Ctxt _ _ _ _ _ (VE_Refl _ hd) tl_vp1
      in
      let d : vprop_equiv g (list_as_vprop (vp0 @ vp1))
                              (tm_star (tm_star hd (list_as_vprop tl)) (list_as_vprop vp1))
            = VE_Trans _ _ _ _ d (VE_Assoc _ _ _ _) in
      d


let list_as_vprop_comm g (vp0 vp1:list term)
  : GTot (vprop_equiv g (list_as_vprop (vp0 @ vp1))
                        (list_as_vprop (vp1 @ vp0)))
  = let d1 : _ = list_as_vprop_append g vp0 vp1 in
    let d2 : _ = VE_Sym _ _ _ (list_as_vprop_append g vp1 vp0) in
    let d1 : _ = VE_Trans _ _ _ _ d1 (VE_Comm _ _ _) in
    VE_Trans _ _ _ _ d1 d2

let list_as_vprop_assoc g (vp0 vp1 vp2:list term)
  : GTot (vprop_equiv g (list_as_vprop (vp0 @ (vp1 @ vp2)))
                        (list_as_vprop ((vp0 @ vp1) @ vp2)))
  = List.Tot.append_assoc vp0 vp1 vp2;
    VE_Refl _ _
    
let list_as_vprop_ctx g (vp0 vp0' vp1 vp1':list term)
                        (d0:vprop_equiv g (list_as_vprop vp0) (list_as_vprop vp0'))
                        (d1: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')))

  = let split_app = list_as_vprop_append _ vp0 vp1 in
    let split_app' = list_as_vprop_append _ vp0' vp1' in
    let ctxt = VE_Ctxt _ _ _ _ _ d0 d1 in
    VE_Trans _ _ _ _ split_app (VE_Trans _ _ _ _ ctxt (VE_Sym _ _ _ split_app'))
  
let list_as_vprop_singleton g
  (p q:term)
  (d:vprop_equiv g p q)
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]))

    g: Pulse.Typing.Env.env ->
    p: Pulse.Syntax.Base.term ->
    q: Pulse.Syntax.Base.term ->
    d: Pulse.Typing.vprop_equiv g p q
  -> Prims.GTot
    (Pulse.Typing.vprop_equiv g
        (Pulse.Typing.Combinators.list_as_vprop [p])
        (Pulse.Typing.Combinators.list_as_vprop [q]))