val should_elim_exists (v: vprop) : T.Tac bool
let should_elim_exists (v:vprop) : T.Tac bool =
  match v.t with
  | Tm_ExistsSL _ _ _ -> true
  | _ -> false
val should_elim_exists (v: vprop) : T.Tac bool
let should_elim_exists (v: vprop) : T.Tac bool =
match v.t with
| Tm_ExistsSL _ _ _ -> true
| _ -> false
Pulse.Checker.Prover.ElimExists.fst.checked
Pulse.Typing.Combinators.fsti.checked Pulse.Typing.fst.checked Pulse.Syntax.fst.checked Pulse.Checker.VPropEquiv.fsti.checked Pulse.Checker.Prover.Base.fsti.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Pulse.Checker.Prover.ElimExists.fst
Pulse.Syntax.Base.vprop Pulse.Syntax.Base.__proj__Mkterm__item__t Pulse.Syntax.Base.universe Pulse.Syntax.Base.binder Pulse.Syntax.Base.term Pulse.Syntax.Base.term' Prims.bool
module Pulse.Checker.Prover.ElimExists

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

module T = FStar.Tactics.V2

open Pulse.Checker.VPropEquiv

open Pulse.Checker.Prover.Base
val should_elim_exists (v: vprop) : T.Tac bool
v: Pulse.Syntax.Base.vprop -> FStar.Tactics.Effect.Tac Prims.bool