val check_prop_validity (g: env) (p: term) (typing: tot_typing g p tm_prop)
    : T.Tac (prop_validity g p)
let check_prop_validity (g:env) (p:term) (typing:tot_typing g p tm_prop): T.Tac (prop_validity g p) =
    Pulse.Checker.Pure.check_prop_validity g p typing
val check_prop_validity (g: env) (p: term) (typing: tot_typing g p tm_prop)
    : T.Tac (prop_validity g p)
let check_prop_validity (g: env) (p: term) (typing: tot_typing g p tm_prop)
    : T.Tac (prop_validity g p) =
Pulse.Checker.Pure.check_prop_validity g p typing
Pulse.Checker.IntroPure.fst.checked
Pulse.Typing.Metatheory.fsti.checked Pulse.Typing.Env.fsti.checked Pulse.Typing.fst.checked Pulse.Syntax.Printer.fsti.checked Pulse.Syntax.fst.checked Pulse.Checker.Pure.fsti.checked Pulse.Checker.Prover.fsti.checked Pulse.Checker.Base.fsti.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Printf.fst.checked FStar.Pervasives.fsti.checked
Pulse.Checker.IntroPure.fst
Pulse.Typing.Env.env Pulse.Syntax.Base.term Pulse.Typing.tot_typing Pulse.Typing.tm_prop Pulse.Checker.Pure.check_prop_validity Pulse.Typing.prop_validity
module Pulse.Checker.IntroPure

open Pulse.Syntax
open Pulse.Typing
open Pulse.Checker.Base
open Pulse.Checker.Prover

module T = FStar.Tactics.V2
module P = Pulse.Syntax.Printer

let check_prop (g:env) (p:term) 
  : T.Tac (p:term & tot_typing g p tm_prop) =
  
  let p0 = p in
  let (| p, p_typing |) = Pulse.Checker.Pure.check_vprop g (tm_pure p) in
  match p.t with
  | Tm_Pure pp ->
    let prop_typing = Pulse.Typing.Metatheory.pure_typing_inversion #_ #pp p_typing in
    (| pp, prop_typing |)
  | _ ->
    fail g None
      (Printf.sprintf "Impossible: check_intro_pure: checking a pure vprop %s returned a non-pure vprop %s,\
                       please file a bug-report"
         (P.term_to_string (tm_pure p0))
         (P.term_to_string p))
val check_prop_validity (g: env) (p: term) (typing: tot_typing g p tm_prop)
    : T.Tac (prop_validity g p)

    g: Pulse.Typing.Env.env ->
    p: Pulse.Syntax.Base.term ->
    typing: Pulse.Typing.tot_typing g p Pulse.Typing.tm_prop
  -> FStar.Tactics.Effect.Tac (Pulse.Typing.prop_validity g p)