val elim_exists_frame
      (#g: env)
      (#ctxt #frame: vprop)
      (ctxt_frame_typing: tot_typing g (ctxt * frame) tm_vprop)
      (uvs: env{disjoint uvs g})
    : T.Tac
    (g': env{env_extends g' g /\ disjoint uvs g'} &
      ctxt': term &
      tot_typing g' (ctxt' * frame) tm_vprop &
      continuation_elaborator g (ctxt * frame) g' (ctxt' * frame))
let elim_exists_frame (#g:env) (#ctxt #frame:vprop)
  (ctxt_frame_typing:tot_typing g (ctxt * frame) tm_vprop)
  (uvs:env { disjoint uvs g })
  : T.Tac (g':env { env_extends g' g /\ disjoint uvs g' } &
           ctxt':term &
           tot_typing g' (ctxt' * frame) tm_vprop &
           continuation_elaborator g (ctxt * frame) g' (ctxt' * frame)) =
  add_elims should_elim_exists mk ctxt_frame_typing uvs
val elim_exists_frame
      (#g: env)
      (#ctxt #frame: vprop)
      (ctxt_frame_typing: tot_typing g (ctxt * frame) tm_vprop)
      (uvs: env{disjoint uvs g})
    : T.Tac
    (g': env{env_extends g' g /\ disjoint uvs g'} &
      ctxt': term &
      tot_typing g' (ctxt' * frame) tm_vprop &
      continuation_elaborator g (ctxt * frame) g' (ctxt' * frame))
let elim_exists_frame
      (#g: env)
      (#ctxt #frame: vprop)
      (ctxt_frame_typing: tot_typing g (ctxt * frame) tm_vprop)
      (uvs: env{disjoint uvs g})
    : T.Tac
    (g': env{env_extends g' g /\ disjoint uvs g'} &
      ctxt': term &
      tot_typing g' (ctxt' * frame) tm_vprop &
      continuation_elaborator g (ctxt * frame) g' (ctxt' * frame)) =
add_elims should_elim_exists mk ctxt_frame_typing uvs
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.Typing.Env.env Pulse.Syntax.Base.vprop Pulse.Typing.tot_typing Pulse.Checker.Prover.Base.op_Star Pulse.Syntax.Base.tm_vprop Pulse.Typing.Env.disjoint Pulse.Checker.Prover.Base.add_elims Pulse.Checker.Prover.ElimExists.should_elim_exists Pulse.Checker.Prover.ElimExists.mk FStar.Pervasives.dtuple4 Prims.l_and Pulse.Typing.Env.env_extends Pulse.Syntax.Base.term Pulse.Syntax.Base.tm_star Pulse.Checker.Base.continuation_elaborator
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

let should_elim_exists (v:vprop) : T.Tac bool =
  match v.t with
  | Tm_ExistsSL _ _ _ -> true
  | _ -> false

let mk (#g:env) (#v:vprop) (v_typing:tot_typing g v tm_vprop)
  : T.Tac (option (x:ppname &
                   t:st_term &
                   c:comp { stateful_comp c /\ comp_pre c == v } &
                   st_typing g t c)) =

  match v.t with
  | Tm_ExistsSL u { binder_ppname=nm; binder_ty = t } p ->
    let x = fresh g in
    let c = Pulse.Typing.comp_elim_exists u t p (nm, x) in
    let tm_typing : st_typing g _ c =
        T_ElimExists g (comp_u c) t p x (magic()) (magic())
    in
    Some (| nm, _, c, tm_typing |)
  | _ -> None

let elim_exists_frame (#g:env) (#ctxt #frame:vprop)
  (ctxt_frame_typing:tot_typing g (ctxt * frame) tm_vprop)
  (uvs:env { disjoint uvs g })
  : T.Tac (g':env { env_extends g' g /\ disjoint uvs g' } &
           ctxt':term &
           tot_typing g' (ctxt' * frame) tm_vprop &
val elim_exists_frame
      (#g: env)
      (#ctxt #frame: vprop)
      (ctxt_frame_typing: tot_typing g (ctxt * frame) tm_vprop)
      (uvs: env{disjoint uvs g})
    : T.Tac
    (g': env{env_extends g' g /\ disjoint uvs g'} &
      ctxt': term &
      tot_typing g' (ctxt' * frame) tm_vprop &
      continuation_elaborator g (ctxt * frame) g' (ctxt' * frame))

    ctxt_frame_typing: Pulse.Typing.tot_typing g (ctxt * frame) Pulse.Syntax.Base.tm_vprop ->
    uvs: Pulse.Typing.Env.env{Pulse.Typing.Env.disjoint uvs g}
  -> FStar.Tactics.Effect.Tac
    (FStar.Pervasives.dtuple4 (g':
          Pulse.Typing.Env.env
            {Pulse.Typing.Env.env_extends g' g /\ Pulse.Typing.Env.disjoint uvs g'})
        (fun _ -> Pulse.Syntax.Base.term)
        (fun g' ctxt' -> Pulse.Typing.tot_typing g' (ctxt' * frame) Pulse.Syntax.Base.tm_vprop)
        (fun g' ctxt' _ ->
            Pulse.Checker.Base.continuation_elaborator g (ctxt * frame) g' (ctxt' * frame)))