val gen_elim_prop_elim
  (enable_nondep_opt: bool)
  (p: vprop)
  (a: Type u#1)
  (q: Ghost.erased a -> Tot vprop)
  (post: Ghost.erased a -> Tot prop)
: Ghost (gen_elim_i & gen_elim_nondep_t)
  (requires gen_elim_prop enable_nondep_opt p a q post)
  (ensures (fun (i, j) ->
    p == compute_gen_elim_p i /\
    check_gen_elim_nondep_sem i j /\
    a == compute_gen_elim_nondep_a i j /\
    q == compute_gen_elim_nondep_q i j /\
    post == compute_gen_elim_nondep_post i j
  ))
let gen_elim_prop_elim enable_nondep_opt p a q post =
  FStar.IndefiniteDescription.indefinite_description_ghost _ (gen_elim_pred enable_nondep_opt p a q post)
val gen_elim_prop_elim
  (enable_nondep_opt: bool)
  (p: vprop)
  (a: Type u#1)
  (q: Ghost.erased a -> Tot vprop)
  (post: Ghost.erased a -> Tot prop)
: Ghost (gen_elim_i & gen_elim_nondep_t)
  (requires gen_elim_prop enable_nondep_opt p a q post)
  (ensures (fun (i, j) ->
    p == compute_gen_elim_p i /\
    check_gen_elim_nondep_sem i j /\
    a == compute_gen_elim_nondep_a i j /\
    q == compute_gen_elim_nondep_q i j /\
    post == compute_gen_elim_nondep_post i j
  ))
let gen_elim_prop_elim enable_nondep_opt p a q post =
FStar.IndefiniteDescription.indefinite_description_ghost _
  (gen_elim_pred enable_nondep_opt p a q post)
Steel.ST.GenElim1.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.GenElim1.Base.fst
Prims.bool Steel.Effect.Common.vprop FStar.Ghost.erased Prims.prop FStar.IndefiniteDescription.indefinite_description_ghost FStar.Pervasives.Native.tuple2 Steel.ST.GenElim1.Base.gen_elim_i Steel.ST.GenElim1.Base.gen_elim_nondep_t Steel.ST.GenElim1.Base.gen_elim_pred
module Steel.ST.GenElim1.Base

irreducible let gen_elim_reduce = ()

[@@noextract_to "Plugin"]
let gen_elim_pred
  (enable_nondep_opt: bool)
  (p: vprop)
  (a: Type u#1)
  (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
  enable_nondep_opt p a q post
= exists ij . gen_elim_pred enable_nondep_opt p a q post ij

let gen_elim_prop_intro'
  i j enable_nondep_opt p a q post sq_p sq_j sq_a sq_q sq_post
= assert (gen_elim_pred enable_nondep_opt p a q post (i, j))
val gen_elim_prop_elim
  (enable_nondep_opt: bool)
  (p: vprop)
  (a: Type u#1)
  (q: Ghost.erased a -> Tot vprop)
  (post: Ghost.erased a -> Tot prop)
: Ghost (gen_elim_i & gen_elim_nondep_t)
  (requires gen_elim_prop enable_nondep_opt p a q post)
  (ensures (fun (i, j) ->
    p == compute_gen_elim_p i /\
    check_gen_elim_nondep_sem i j /\
    a == compute_gen_elim_nondep_a i j /\
    q == compute_gen_elim_nondep_q i j /\
    post == compute_gen_elim_nondep_post i j
  ))

    enable_nondep_opt: Prims.bool ->
    p: Steel.Effect.Common.vprop ->
    a: Type ->
    q: (_: FStar.Ghost.erased a -> Steel.Effect.Common.vprop) ->
    post: (_: FStar.Ghost.erased a -> Prims.prop)
  -> Prims.Ghost (Steel.ST.GenElim1.Base.gen_elim_i * Steel.ST.GenElim1.Base.gen_elim_nondep_t)