let vprop_typing (g:env) (t:term) = tot_typing g t tm_vprop
let vprop_typing (g: env) (t: term) =
tot_typing g t tm_vprop
Pulse.Checker.Prover.Base.fsti.checked
Pulse.Typing.Combinators.fsti.checked Pulse.Typing.fst.checked Pulse.Syntax.fst.checked Pulse.Checker.Prover.Substs.fsti.checked Pulse.Checker.Base.fsti.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Set.fsti.checked FStar.Pervasives.fsti.checked
Pulse.Checker.Prover.Base.fsti
Pulse.Typing.Env.env Pulse.Syntax.Base.term Pulse.Typing.tot_typing Pulse.Syntax.Base.tm_vprop
module Pulse.Checker.Prover.Base

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

open Pulse.Checker.Base

module T = FStar.Tactics.V2
module PS = Pulse.Checker.Prover.Substs
val vprop_typing : g: Pulse.Typing.Env.env -> t: Pulse.Syntax.Base.term -> Type0
g: Pulse.Typing.Env.env -> t: Pulse.Syntax.Base.term -> Type0