val compute_gen_elim_f_exists_no_abs (a: Type0) (body: (a -> vprop))
    : GTot (gen_elim_t (GEExistsNoAbs body))
let compute_gen_elim_f_exists_no_abs
  (a: Type0)
  (body: (a -> vprop))
: GTot (gen_elim_t (GEExistsNoAbs body))
= fun _ ->
  rewrite (compute_gen_elim_p (GEExistsNoAbs body)) (exists_ body);
  let gres = elim_exists () in
  let res : compute_gen_elim_a (GEExistsNoAbs body) = coerce_with_trefl (Ghost.reveal gres) in
  rewrite (body gres) (compute_gen_elim_q (GEExistsNoAbs body) res);
  res
val compute_gen_elim_f_exists_no_abs (a: Type0) (body: (a -> vprop))
    : GTot (gen_elim_t (GEExistsNoAbs body))
let compute_gen_elim_f_exists_no_abs (a: Type0) (body: (a -> vprop))
    : GTot (gen_elim_t (GEExistsNoAbs body)) =
fun _ ->
  rewrite (compute_gen_elim_p (GEExistsNoAbs body)) (exists_ body);
  let gres = elim_exists () in
  let res:compute_gen_elim_a (GEExistsNoAbs body) = coerce_with_trefl (Ghost.reveal gres) in
  rewrite (body gres) (compute_gen_elim_q (GEExistsNoAbs body) res);
  res
Steel.ST.GenElim.fst.checked
prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked FStar.Classical.fsti.checked
Steel.ST.GenElim.fst
Steel.Effect.Common.vprop Steel.Memory.inames Steel.ST.GenElim.Base.compute_gen_elim_a Steel.ST.GenElim.Base.GEExistsNoAbs Prims.unit Steel.ST.Util.rewrite FStar.Ghost.reveal Steel.ST.GenElim.Base.compute_gen_elim_q Steel.ST.GenElim.Base.coerce_with_trefl FStar.Ghost.erased Steel.ST.Util.elim_exists Steel.ST.GenElim.Base.compute_gen_elim_p Steel.ST.Util.exists_ Steel.ST.GenElim.gen_elim_t
module Steel.ST.GenElim

let gen_elim_f
  (p: vprop)
  (a: Type0) // FIXME: generalize this universe
  (q: (a -> vprop))
  (post: (a -> prop))
: Tot Type
= ((opened: inames) -> STGhost a opened p q True post)

let gen_unit_elim_t (i: gen_unit_elim_i) : Tot Type =
  gen_elim_f (compute_gen_unit_elim_p i) unit (fun _ -> compute_gen_unit_elim_q i) (fun _ -> compute_gen_unit_elim_post i)

let compute_gen_unit_elim_f_id
  (v: vprop)
: Tot (gen_unit_elim_t (GUEId v))
= fun _ -> noop ()

let compute_gen_unit_elim_f_pure
  (p: prop)
: Tot (gen_unit_elim_t (GUEPure p))
= fun _ ->
  rewrite (compute_gen_unit_elim_p (GUEPure p)) (pure p);
  elim_pure p

let compute_gen_unit_elim_f_star
  (i1 i2: gen_unit_elim_i)
  (f1: gen_unit_elim_t i1)
  (f2: gen_unit_elim_t i2)
: Tot (gen_unit_elim_t (GUEStar i1 i2))
= fun _ ->
  rewrite (compute_gen_unit_elim_p (GUEStar i1 i2)) (compute_gen_unit_elim_p i1 `star` compute_gen_unit_elim_p i2);
  f1 _; f2 _;
  rewrite (compute_gen_unit_elim_q i1 `star` compute_gen_unit_elim_q i2) (compute_gen_unit_elim_q (GUEStar i1 i2))

let rec compute_gen_unit_elim_f
  (i: gen_unit_elim_i)
: GTot (gen_unit_elim_t i)
= match i returns (gen_unit_elim_t i) with
  | GUEId v -> compute_gen_unit_elim_f_id v
  | GUEPure p -> compute_gen_unit_elim_f_pure p
  | GUEStar i1 i2 -> compute_gen_unit_elim_f_star i1 i2 (compute_gen_unit_elim_f i1) (compute_gen_unit_elim_f i2)

let gen_elim_t (i: gen_elim_i) : Tot Type =
  gen_elim_f (compute_gen_elim_p i) (compute_gen_elim_a i) (compute_gen_elim_q i) (compute_gen_elim_post i)

let compute_gen_elim_f_unit
  (i: gen_unit_elim_i)
: GTot (gen_elim_t (GEUnit i))
= compute_gen_unit_elim_f i

let compute_gen_elim_f_star_l
  (i1: gen_elim_i)
  (f1: gen_elim_t i1)
  (i2: gen_unit_elim_i)
: GTot (gen_elim_t (GEStarL i1 i2))
= let f2 = compute_gen_unit_elim_f i2 in
  fun _ ->
  rewrite (compute_gen_elim_p (GEStarL i1 i2)) (compute_gen_elim_p i1 `star` compute_gen_unit_elim_p i2);
  let res = f1 _ in
  f2 _;
  let res' : compute_gen_elim_a (GEStarL i1 i2) = coerce_with_trefl res in
  rewrite (compute_gen_elim_q i1 res `star` compute_gen_unit_elim_q i2) (compute_gen_elim_q (GEStarL i1 i2) res');
  res'

let compute_gen_elim_f_star_r
  (i1: gen_unit_elim_i)
  (i2: gen_elim_i)
  (f2: gen_elim_t i2)
: GTot (gen_elim_t (GEStarR i1 i2))
= let f1 = compute_gen_unit_elim_f i1 in
  fun _ ->
  rewrite (compute_gen_elim_p (GEStarR i1 i2)) (compute_gen_unit_elim_p i1 `star` compute_gen_elim_p i2);
  f1 _;
  let res = f2 _ in
  let res' : compute_gen_elim_a (GEStarR i1 i2) = coerce_with_trefl res in
  rewrite (compute_gen_unit_elim_q i1 `star` compute_gen_elim_q i2 res) (compute_gen_elim_q (GEStarR i1 i2) res');
  res'

let compute_gen_elim_f_star
  (i1: gen_elim_i)
  (f1: gen_elim_t i1)
  (i2: gen_elim_i)
  (f2: gen_elim_t i2)
: GTot (gen_elim_t (GEStar i1 i2))
= fun _ ->
  rewrite (compute_gen_elim_p (GEStar i1 i2)) (compute_gen_elim_p i1 `star` compute_gen_elim_p i2);
  let res1 = f1 _ in
  let res2 = f2 _ in
  let res : compute_gen_elim_a (GEStar i1 i2) = coerce_with_trefl (res1, res2) in
  rewrite (compute_gen_elim_q i1 res1 `star` compute_gen_elim_q i2 res2) (compute_gen_elim_q (GEStar i1 i2) res);
  res

let compute_gen_elim_f_exists_no_abs
  (a: Type0)
  (body: (a -> vprop))
val compute_gen_elim_f_exists_no_abs (a: Type0) (body: (a -> vprop))
    : GTot (gen_elim_t (GEExistsNoAbs body))
a: Type0 -> body: (_: a -> Steel.Effect.Common.vprop)
  -> Prims.GTot (Steel.ST.GenElim.gen_elim_t (Steel.ST.GenElim.Base.GEExistsNoAbs body))