val 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))
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))
val 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))
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))
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.ST.GenElim.Base.gen_unit_elim_i Steel.ST.GenElim.gen_unit_elim_t Steel.Memory.inames Steel.ST.Util.rewrite Steel.Effect.Common.star Steel.ST.GenElim.Base.compute_gen_unit_elim_q Steel.ST.GenElim.Base.GUEStar Prims.unit Steel.ST.GenElim.Base.compute_gen_unit_elim_p
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)
val 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))

    i1: Steel.ST.GenElim.Base.gen_unit_elim_i ->
    i2: Steel.ST.GenElim.Base.gen_unit_elim_i ->
    f1: Steel.ST.GenElim.gen_unit_elim_t i1 ->
    f2: Steel.ST.GenElim.gen_unit_elim_t i2
  -> Steel.ST.GenElim.gen_unit_elim_t (Steel.ST.GenElim.Base.GUEStar i1 i2)