val compute_gen_unit_elim_f_pure (p: prop) : Tot (gen_unit_elim_t (GUEPure p))
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
val compute_gen_unit_elim_f_pure (p: prop) : Tot (gen_unit_elim_t (GUEPure p))
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
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
Prims.prop Steel.Memory.inames Steel.ST.Util.elim_pure Prims.unit Steel.ST.Util.rewrite Steel.ST.GenElim.Base.compute_gen_unit_elim_p Steel.ST.GenElim.Base.GUEPure Steel.ST.Util.pure Steel.ST.GenElim.gen_unit_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)
val compute_gen_unit_elim_f_pure (p: prop) : Tot (gen_unit_elim_t (GUEPure p))
p: Prims.prop -> Steel.ST.GenElim.gen_unit_elim_t (Steel.ST.GenElim.Base.GUEPure p)