val canon_vprop (vp: term) : term
let canon_vprop (vp:term)
  : term
  = list_as_vprop (vprop_as_list vp)
val canon_vprop (vp: term) : term
let canon_vprop (vp: term) : term =
list_as_vprop (vprop_as_list vp)
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.Syntax.Base.term Pulse.Typing.Combinators.list_as_vprop Pulse.Typing.Combinators.vprop_as_list
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)
val canon_vprop (vp: term) : term
vp: Pulse.Syntax.Base.term -> Pulse.Syntax.Base.term