val compute_gen_elim_a (x: gen_elim_i) : Tot Type0
let rec compute_gen_elim_a
  (x: gen_elim_i)
: Tot Type0
= match x with
  | GEUnit _ -> unit
  | GEStarL left _ -> compute_gen_elim_a left
  | GEStarR _ right -> compute_gen_elim_a right
  | GEStar left right -> (compute_gen_elim_a left & compute_gen_elim_a right)
  | GEExistsNoAbs #a _
  | GEExistsUnit #a _ -> a
  | GEExists #a body -> dtuple2 a (fun x -> compute_gen_elim_a (body x))
val compute_gen_elim_a (x: gen_elim_i) : Tot Type0
let rec compute_gen_elim_a (x: gen_elim_i) : Tot Type0 =
match x with
| GEUnit _ -> unit
| GEStarL left _ -> compute_gen_elim_a left
| GEStarR _ right -> compute_gen_elim_a right
| GEStar left right -> (compute_gen_elim_a left & compute_gen_elim_a right)
| GEExistsNoAbs #a _ | GEExistsUnit #a _ -> a
| GEExists #a body -> dtuple2 a (fun x -> compute_gen_elim_a (body x))
Steel.ST.GenElim.Base.fsti.checked
Steel.ST.Util.fsti.checked Steel.Effect.Common.fsti.checked prims.fst.checked FStar.Tactics.fst.checked FStar.Reflection.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Ghost.fsti.checked
Steel.ST.GenElim.Base.fsti
Steel.ST.GenElim.Base.gen_elim_i Steel.ST.GenElim.Base.gen_unit_elim_i Prims.unit Steel.ST.GenElim.Base.compute_gen_elim_a FStar.Pervasives.Native.tuple2 Steel.Effect.Common.vprop Prims.dtuple2
module Steel.ST.GenElim.Base
include Steel.ST.Util

module T = FStar.Tactics

let is_fvar     = Reflection.is_fvar
let is_any_fvar = Reflection.is_any_fvar

/// A tactic to automatically generate a unique binder

[@@erasable]
noeq
type gen_unit_elim_i
= | GUEId: (v: vprop) -> gen_unit_elim_i
  | GUEPure: (p: prop) -> gen_unit_elim_i
  | GUEStar: (left: gen_unit_elim_i) -> (right: gen_unit_elim_i) -> gen_unit_elim_i

[@@erasable]
noeq
type gen_elim_i =
  | GEUnit: (i: gen_unit_elim_i) -> gen_elim_i
  | GEStarL: (left: gen_elim_i) -> (right: gen_unit_elim_i) -> gen_elim_i
  | GEStarR: (left: gen_unit_elim_i) -> (right: gen_elim_i) -> gen_elim_i
  | GEStar: (left: gen_elim_i) -> (right: gen_elim_i) -> gen_elim_i
  | GEExistsNoAbs: (#a: Type0) -> (body: (a -> vprop)) -> gen_elim_i // FIXME: generalize the universe
  | GEExistsUnit: (#a: Type0) -> (body: (a -> gen_unit_elim_i)) -> gen_elim_i
  | GEExists: (#a: Type0) -> (body: (a -> gen_elim_i)) -> gen_elim_i

val gen_elim_reduce: unit

[@@ gen_elim_reduce]
let rec compute_gen_unit_elim_p
  (x: gen_unit_elim_i)
: Tot vprop
= match x with
  | GUEId v -> v
  | GUEPure p -> pure p
  | GUEStar left right -> compute_gen_unit_elim_p left `star` compute_gen_unit_elim_p right

[@@ gen_elim_reduce]
let rec compute_gen_unit_elim_q
  (x: gen_unit_elim_i)
: Tot vprop
= match x with
  | GUEId v -> v
  | GUEPure _ -> emp
  | GUEStar left right -> compute_gen_unit_elim_q left `star` compute_gen_unit_elim_q right

[@@gen_elim_reduce; noextract_to "Plugin"]
let rec compute_gen_unit_elim_post
  (x: gen_unit_elim_i)
: Tot prop
= match x with
  | GUEId _ -> True
  | GUEPure p -> p
  | GUEStar left right -> compute_gen_unit_elim_post left /\ compute_gen_unit_elim_post right

[@@gen_elim_reduce]
let rec compute_gen_elim_p
  (x: gen_elim_i)
: Tot vprop
= match x with
  | GEUnit i -> compute_gen_unit_elim_p i
  | GEStarL left right -> compute_gen_elim_p left `star` compute_gen_unit_elim_p right
  | GEStarR left right -> compute_gen_unit_elim_p left `star` compute_gen_elim_p right
  | GEStar left right -> compute_gen_elim_p left `star` compute_gen_elim_p right
  | GEExistsNoAbs #a p -> exists_ p
  | GEExistsUnit #a p -> exists_ (fun x -> compute_gen_unit_elim_p (p x))
  | GEExists #a body -> exists_ (fun x -> compute_gen_elim_p (body x))

let compute_gen_elim_p' = compute_gen_elim_p

[@@ gen_elim_reduce; __steel_reduce__; noextract_to "Plugin"]
let rec compute_gen_elim_a
  (x: gen_elim_i)
val compute_gen_elim_a (x: gen_elim_i) : Tot Type0
x: Steel.ST.GenElim.Base.gen_elim_i -> Type0