val gen_elim_prop
  (enable_nondep_opt: bool)
  (p: vprop)
  (a: Type0)
  (q: Ghost.erased a -> Tot vprop)
  (post: Ghost.erased a -> Tot prop)
: Tot prop
let gen_elim_prop
  enable_nondep_opt p a q post
= exists ij . gen_elim_pred enable_nondep_opt p a q post ij
val gen_elim_prop
  (enable_nondep_opt: bool)
  (p: vprop)
  (a: Type0)
  (q: Ghost.erased a -> Tot vprop)
  (post: Ghost.erased a -> Tot prop)
: Tot prop
let gen_elim_prop enable_nondep_opt p a q post =
exists ij. gen_elim_pred enable_nondep_opt p a q post ij
Steel.ST.GenElim.Base.fst.checked
prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.IndefiniteDescription.fsti.checked FStar.Ghost.fsti.checked
Steel.ST.GenElim.Base.fst
Prims.bool Steel.Effect.Common.vprop FStar.Ghost.erased Prims.prop Prims.l_Exists FStar.Pervasives.Native.tuple2 Steel.ST.GenElim.Base.gen_elim_i Steel.ST.GenElim.Base.gen_elim_nondep_t Steel.ST.GenElim.Base.gen_elim_pred
module Steel.ST.GenElim.Base

irreducible let gen_elim_reduce = ()

[@@noextract_to "Plugin"]
let gen_elim_pred
  (enable_nondep_opt: bool)
  (p: vprop)
  (a: Type0)
  (q: Ghost.erased a -> Tot vprop)
  (post: Ghost.erased a -> Tot prop)
  (ij: (gen_elim_i & gen_elim_nondep_t))
: Tot prop
= let (i, j) = ij in
  p == compute_gen_elim_p i /\
  check_gen_elim_nondep_sem i j /\ 
  a == compute_gen_elim_nondep_a i j /\
  post == compute_gen_elim_nondep_post i j /\
  q == compute_gen_elim_nondep_q i j

let gen_elim_prop
val gen_elim_prop
  (enable_nondep_opt: bool)
  (p: vprop)
  (a: Type0)
  (q: Ghost.erased a -> Tot vprop)
  (post: Ghost.erased a -> Tot prop)
: Tot prop

    enable_nondep_opt: Prims.bool ->
    p: Steel.Effect.Common.vprop ->
    a: Type0 ->
    q: (_: FStar.Ghost.erased a -> Steel.Effect.Common.vprop) ->
    post: (_: FStar.Ghost.erased a -> Prims.prop)
  -> Prims.prop