val ve_unit_r (g:env) (p:term) : vprop_equiv g (tm_star p tm_emp) p
let ve_unit_r g (p:term) : vprop_equiv g (tm_star p tm_emp) p = 
  VE_Trans _ _ _ _ (VE_Comm _ _ _) (VE_Unit _ _)
val ve_unit_r (g:env) (p:term) : vprop_equiv g (tm_star p tm_emp) p
let ve_unit_r g (p: term) : vprop_equiv g (tm_star p tm_emp) p =
VE_Trans _ _ _ _ (VE_Comm _ _ _) (VE_Unit _ _)
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.VE_Trans Pulse.Syntax.Base.tm_star Pulse.Syntax.Base.tm_emp Pulse.Typing.VE_Comm Pulse.Typing.VE_Unit Pulse.Typing.vprop_equiv
module Pulse.Checker.VPropEquiv
open Pulse.Syntax
open Pulse.Typing
open FStar.List.Tot
val ve_unit_r (g:env) (p:term) : vprop_equiv g (tm_star p tm_emp) p
g: Pulse.Typing.Env.env -> p: Pulse.Syntax.Base.term
  -> Pulse.Typing.vprop_equiv g (Pulse.Syntax.Base.tm_star p Pulse.Syntax.Base.tm_emp) p