val gen_elim_prop_intro'
  (i: gen_elim_i)
  (j: gen_elim_nondep_t)
  (enable_nondep_opt: bool)
  (p: vprop)
  (a: Type u#1)
  (q: Ghost.erased a -> Tot vprop)
  (post: Ghost.erased a -> Tot prop)
  (sq_p: squash (p == compute_gen_elim_p i))
  (sq_j: squash (check_gen_elim_nondep_sem i j))
  (sq_a: squash (a == compute_gen_elim_nondep_a i j))
  (sq_q: squash (q == compute_gen_elim_nondep_q i j))
  (sq_post: squash (post == compute_gen_elim_nondep_post i j))
: Lemma
  (gen_elim_prop enable_nondep_opt p a q post)
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_intro'
  (i: gen_elim_i)
  (j: gen_elim_nondep_t)
  (enable_nondep_opt: bool)
  (p: vprop)
  (a: Type u#1)
  (q: Ghost.erased a -> Tot vprop)
  (post: Ghost.erased a -> Tot prop)
  (sq_p: squash (p == compute_gen_elim_p i))
  (sq_j: squash (check_gen_elim_nondep_sem i j))
  (sq_a: squash (a == compute_gen_elim_nondep_a i j))
  (sq_q: squash (q == compute_gen_elim_nondep_q i j))
  (sq_post: squash (post == compute_gen_elim_nondep_post i j))
: Lemma
  (gen_elim_prop enable_nondep_opt p a q post)
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))
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
Steel.ST.GenElim1.Base.gen_elim_i Steel.ST.GenElim1.Base.gen_elim_nondep_t Prims.bool Steel.Effect.Common.vprop FStar.Ghost.erased Prims.prop Prims.squash Prims.eq2 Steel.ST.GenElim1.Base.compute_gen_elim_p Steel.ST.GenElim1.Base.check_gen_elim_nondep_sem Steel.ST.GenElim1.Base.compute_gen_elim_nondep_a Steel.ST.GenElim1.Base.compute_gen_elim_nondep_q Steel.ST.GenElim1.Base.compute_gen_elim_nondep_post Prims._assert Steel.ST.GenElim1.Base.gen_elim_pred FStar.Pervasives.Native.Mktuple2 Prims.unit
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'
val gen_elim_prop_intro'
  (i: gen_elim_i)
  (j: gen_elim_nondep_t)
  (enable_nondep_opt: bool)
  (p: vprop)
  (a: Type u#1)
  (q: Ghost.erased a -> Tot vprop)
  (post: Ghost.erased a -> Tot prop)
  (sq_p: squash (p == compute_gen_elim_p i))
  (sq_j: squash (check_gen_elim_nondep_sem i j))
  (sq_a: squash (a == compute_gen_elim_nondep_a i j))
  (sq_q: squash (q == compute_gen_elim_nondep_q i j))
  (sq_post: squash (post == compute_gen_elim_nondep_post i j))
: Lemma
  (gen_elim_prop enable_nondep_opt p a q post)

    i: Steel.ST.GenElim1.Base.gen_elim_i ->
    j: Steel.ST.GenElim1.Base.gen_elim_nondep_t ->
    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) ->
    sq_p: Prims.squash (p == Steel.ST.GenElim1.Base.compute_gen_elim_p i) ->
    sq_j: Prims.squash (Steel.ST.GenElim1.Base.check_gen_elim_nondep_sem i j) ->
    sq_a: Prims.squash (a == Steel.ST.GenElim1.Base.compute_gen_elim_nondep_a i j) ->
    sq_q: Prims.squash (q == Steel.ST.GenElim1.Base.compute_gen_elim_nondep_q i j) ->
    sq_post: Prims.squash (post == Steel.ST.GenElim1.Base.compute_gen_elim_nondep_post i j)
  -> FStar.Pervasives.Lemma
    (ensures Steel.ST.GenElim1.Base.gen_elim_prop enable_nondep_opt p a q post)