val 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 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
val 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 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
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 FStar.Pervasives.Native.tuple2 Steel.ST.GenElim.Base.gen_elim_i Steel.ST.GenElim.Base.gen_elim_nondep_t Prims.l_and Prims.eq2 Steel.ST.GenElim.Base.compute_gen_elim_p Steel.ST.GenElim.Base.check_gen_elim_nondep_sem Steel.ST.GenElim.Base.compute_gen_elim_nondep_a Steel.ST.GenElim.Base.compute_gen_elim_nondep_post Steel.ST.GenElim.Base.compute_gen_elim_nondep_q
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))
val 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

    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) ->
    ij: (Steel.ST.GenElim.Base.gen_elim_i * Steel.ST.GenElim.Base.gen_elim_nondep_t)
  -> Prims.prop