val gen_elim_nondep_sem (ty: list (Type u#a))
    : Tot
    (
          curried_function_type ty (U.raise_t u#_ u#(max 2 a) unit -> vprop) ->
          curried_function_type ty (U.raise_t u#_ u#(max 2 a) unit -> prop)
        -> Tot (gen_elim_tele u#a))
val gen_elim_nondep_sem (ty: list (Type u#a))
    : Tot
    (
          curried_function_type ty (U.raise_t u#_ u#(max 2 a) unit -> vprop) ->
          curried_function_type ty (U.raise_t u#_ u#(max 2 a) unit -> prop)
        -> Tot (gen_elim_tele u#a))
let rec gen_elim_nondep_sem (ty: list (Type u#a)) : Tot (curried_function_type ty (U.raise_t u#_ u#(max 2 a) unit -> vprop) -> curried_function_type ty (U.raise_t u#_ u#(max 2 a) unit -> prop) -> Tot (gen_elim_tele u#a)) =
  match ty as ty' returns curried_function_type ty' (U.raise_t u#_ u#(max 2 a) unit -> vprop) -> curried_function_type ty' (U.raise_t u#_ u#(max 2 a) unit -> prop) -> Tot gen_elim_tele with
  | [] -> fun q post -> TRet (q (U.raise_val ())) (post (U.raise_val ()))
  | t :: tq -> fun q post -> TExists t (fun x -> gen_elim_nondep_sem tq (q x) (post x))
module Steel.ST.GenElim1.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
  | GEExistsNoAbs0: (#a: Type0) -> (body: (a -> vprop)) -> gen_elim_i // FIXME: generalize the universe
  | GEExistsUnit0: (#a: Type0) -> (body: (a -> gen_unit_elim_i)) -> gen_elim_i
  | GEExists0: (#a: Type0) -> (body: (a -> gen_elim_i)) -> gen_elim_i
  | GEExistsNoAbs1: (#a: Type u#1) -> (body: (a -> vprop)) -> gen_elim_i // FIXME: generalize the universe
  | GEExistsUnit1: (#a: Type u#1) -> (body: (a -> gen_unit_elim_i)) -> gen_elim_i
  | GEExists1: (#a: Type u#1) -> (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
  | GEExistsNoAbs0 #a p -> exists_ p
  | GEExistsUnit0 #a p -> exists_ (fun x -> compute_gen_unit_elim_p (p x))
  | GEExists0 #a body -> exists_ (fun x -> compute_gen_elim_p (body x))
  | GEExistsNoAbs1 #a p -> exists_ p
  | GEExistsUnit1 #a p -> exists_ (fun x -> compute_gen_unit_elim_p (p x))
  | GEExists1 #a body -> exists_ (fun x -> compute_gen_elim_p (body x))

let compute_gen_elim_p' = compute_gen_elim_p

module U = FStar.Universe

[@@ gen_elim_reduce; __steel_reduce__; noextract_to "Plugin"]
let rec compute_gen_elim_a
  (x: gen_elim_i)
: Tot (Type u#1)
= match x with
  | GEUnit _ -> U.raise_t 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)
  | GEExistsNoAbs0 #a _
  | GEExistsUnit0 #a _ -> U.raise_t a
  | GEExists0 #a body -> dtuple2 a (fun x -> compute_gen_elim_a (body x))
  | GEExistsNoAbs1 #a _
  | GEExistsUnit1 #a _ -> a
  | GEExists1 #a body -> dtuple2 a (fun x -> compute_gen_elim_a (body x))

[@@noextract_to "Plugin"]
let dfstp #a #b t = dfst #a #b t
[@@noextract_to "Plugin"]
let dsndp #a #b t = dsnd #a #b t
[@@noextract_to "Plugin"]
let fstp #a #b t = fst #a #b t
[@@noextract_to "Plugin"]
let sndp #a #b t = snd #a #b t

[@@gen_elim_reduce; __steel_reduce__; noextract_to "Plugin"]
let coerce_with_trefl (#tfrom #tto: Type) (x: tfrom) : Pure tto (requires (T.with_tactic T.trefl (tfrom == tto))) (ensures (fun _ -> True)) = x

[@@gen_elim_reduce]
let rec compute_gen_elim_q
  (x: gen_elim_i)
: Tot (compute_gen_elim_a x -> Tot vprop)
  (decreases x)
= match x as x' returns (compute_gen_elim_a x' -> Tot vprop) with
  | GEUnit u -> fun _ -> compute_gen_unit_elim_q u
  | GEStarL left right -> fun v -> compute_gen_elim_q left (coerce_with_trefl v) `star` compute_gen_unit_elim_q right
  | GEStarR left right -> fun v -> compute_gen_unit_elim_q left `star` compute_gen_elim_q right (coerce_with_trefl v)
  | GEStar left right ->
    let tleft = compute_gen_elim_a left in
    let tright = compute_gen_elim_a right in
    fun v ->
      let v' : (tleft & tright) = coerce_with_trefl v in
      compute_gen_elim_q left (fstp #tleft #tright v') `star` compute_gen_elim_q right (sndp #tleft #tright v')
  | GEExistsNoAbs0 #a p -> fun v -> p (U.downgrade_val v)
  | GEExistsUnit0 #a p -> fun v -> compute_gen_unit_elim_q (p (U.downgrade_val v))
  | GEExists0 #a body ->
    let dept = (fun x -> compute_gen_elim_a (body x)) in
    fun v ->
    let v' : dtuple2 a dept = coerce_with_trefl v in
    compute_gen_elim_q
      (body (dfstp #a #dept v'))
      (dsndp #a #dept v')
  | GEExistsNoAbs1 #a p -> p
  | GEExistsUnit1 #a p -> fun v -> compute_gen_unit_elim_q (p v)
  | GEExists1 #a body ->
    let dept = (fun x -> compute_gen_elim_a (body x)) in
    fun v ->
    let v' : dtuple2 a dept = coerce_with_trefl v in
    compute_gen_elim_q
      (body (dfstp #a #dept v'))
      (dsndp #a #dept v')

[@@gen_elim_reduce; noextract_to "Plugin"]
let rec compute_gen_elim_post
  (x: gen_elim_i)
: Tot (compute_gen_elim_a x -> Tot prop)
  (decreases x)
= match x as x' returns (compute_gen_elim_a x' -> Tot prop) with
  | GEUnit u -> fun _ -> compute_gen_unit_elim_post u
  | GEStarL left right -> fun v -> compute_gen_elim_post left (coerce_with_trefl v) /\ compute_gen_unit_elim_post right
  | GEStarR left right -> fun v -> compute_gen_unit_elim_post left /\ compute_gen_elim_post right (coerce_with_trefl v)
  | GEStar left right ->
    let tleft = compute_gen_elim_a left in
    let tright = compute_gen_elim_a right in
    fun v ->
      let v' : (tleft & tright) = coerce_with_trefl v in
      compute_gen_elim_post left (fstp #tleft #tright v') /\ compute_gen_elim_post right (sndp #tleft #tright v')
  | GEExistsNoAbs0 #a p -> fun _ -> True
  | GEExistsUnit0 #a p -> fun v -> compute_gen_unit_elim_post (p (U.downgrade_val v))
  | GEExists0 #a body ->
    let dept = (fun x -> compute_gen_elim_a (body x)) in
    fun v ->
    let v' : dtuple2 a dept = coerce_with_trefl v in
    compute_gen_elim_post
      (body (dfstp #a #dept v'))
      (dsndp #a #dept v')
  | GEExistsNoAbs1 #a p -> fun _ -> True
  | GEExistsUnit1 #a p -> fun v -> compute_gen_unit_elim_post (p v)
  | GEExists1 #a body ->
    let dept = (fun x -> compute_gen_elim_a (body x)) in
    fun v ->
    let v' : dtuple2 a dept = coerce_with_trefl v in
    compute_gen_elim_post
      (body (dfstp #a #dept v'))
      (dsndp #a #dept v')

[@@erasable]
noeq
type gen_elim_tele : Type u#(max 2 (a + 1)) =
  | TRet: vprop -> prop -> gen_elim_tele
  | TExists: (ty: Type u#a) -> (ty -> gen_elim_tele) -> gen_elim_tele

[@@gen_elim_reduce]
let rec tele_star_vprop (i: gen_elim_tele) (v: vprop) (p: prop) : Tot gen_elim_tele (decreases i) =
  match i with
  | TRet v' p' -> TRet (v `star` v') (p /\ p')
  | TExists ty f -> TExists ty (fun x -> tele_star_vprop (f x) v p)

[@@gen_elim_reduce]
let rec tele_star (i1 i2: gen_elim_tele) : Tot gen_elim_tele =
  match i1, i2 with
  | TRet v1 p1, _ -> tele_star_vprop i2 v1 p1
  | _, TRet v2 p2 -> tele_star_vprop i1 v2 p2
  | TExists ty1 f1, TExists ty2 f2 -> TExists ty1 (fun x1 -> TExists ty2 (fun x2 -> tele_star (f1 x1) (f2 x2)))

[@@gen_elim_reduce]
let rec compute_gen_elim_tele (x: gen_elim_i) : Tot (gen_elim_tele u#1) =
  match x with
  | GEUnit v -> TRet (compute_gen_unit_elim_q v) (compute_gen_unit_elim_post v)
  | GEStarL l ru -> tele_star_vprop (compute_gen_elim_tele l) (compute_gen_unit_elim_q ru) (compute_gen_unit_elim_post ru)
  | GEStarR lu r -> tele_star_vprop (compute_gen_elim_tele r) (compute_gen_unit_elim_q lu) (compute_gen_unit_elim_post lu)
  | GEStar l r -> tele_star (compute_gen_elim_tele l) (compute_gen_elim_tele r)
  | GEExistsNoAbs0 #ty body -> TExists (U.raise_t ty) (fun x -> TRet (body (U.downgrade_val x)) True)
  | GEExistsUnit0 #ty body -> TExists (U.raise_t ty) (fun x -> TRet (compute_gen_unit_elim_q (body (U.downgrade_val x))) (compute_gen_unit_elim_post (body (U.downgrade_val x))))
  | GEExists0 #ty f -> TExists (U.raise_t ty) (fun x -> compute_gen_elim_tele (f (U.downgrade_val x)))
  | GEExistsNoAbs1 #ty body -> TExists ty (fun x -> TRet (body x) True)
  | GEExistsUnit1 #ty body -> TExists ty (fun x -> TRet (compute_gen_unit_elim_q (body x)) (compute_gen_unit_elim_post (body x)))
  | GEExists1 #ty f -> TExists ty (fun x -> compute_gen_elim_tele (f x))

[@@gen_elim_reduce; noextract_to "Plugin"]
let rec curried_function_type (x: list (Type u#a)) (ret_t: Type u#(max a b)) : Tot (Type u#(max a b)) =
  match x with
  | [] -> ret_t
  | t1 :: q -> t1 -> Tot (curried_function_type q ret_t)

[@@erasable]
noeq
type gen_elim_nondep_t : Type u#(max 2 (a + 1)) =
| GENonDep: (ty: list (Type u#a)) -> curried_function_type ty (U.raise_t u#_ u#(max 2 a) unit -> vprop) -> curried_function_type ty (U.raise_t u#_ u#(max 2 a) unit -> prop) -> gen_elim_nondep_t
| GEDep

[@@gen_elim_reduce]
let mk_gen_elim_nondep
  (ty: list (Type u#a))
  (tvprop: Type)
  (q: tvprop)
  (tprop: Type)
  (post: tprop)
: Pure (gen_elim_nondep_t u#a)
  (requires (
    tvprop == curried_function_type ty (U.raise_t u#_ u#(max 2 a) unit -> vprop) /\
    tprop == curried_function_type ty (U.raise_t u#_ u#(max 2 a) unit -> prop)
  ))
  (ensures (fun _ -> True))
= GENonDep ty q post

[@@gen_elim_reduce]
let mk_gen_elim_nondep_by_tac
  (ty: list (Type u#a))
  (tvprop: Type)
  (q: tvprop)
  (tprop: Type)
  (post: tprop)
: Pure (gen_elim_nondep_t u#a)
  (requires (
    T.with_tactic (fun _ -> T.norm [delta_attr [(`%gen_elim_reduce)]; iota; zeta]) (tvprop == curried_function_type ty (U.raise_t u#_ u#(max 2 a) unit -> vprop)) /\
    T.with_tactic (fun _ -> T.norm [delta_attr [(`%gen_elim_reduce)]; iota; zeta]) (tprop == curried_function_type ty (U.raise_t u#_ u#(max 2 a) unit -> prop))
  ))
  (ensures (fun _ -> True))
= GENonDep ty q post
/
Steel.ST.Util.fsti.checked Steel.Effect.Common.fsti.checked prims.fst.checked FStar.Universe.fsti.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.GenElim1.Base.fsti

    ty: Prims.list Type ->
    _:
      Steel.ST.GenElim1.Base.curried_function_type ty
        (_: FStar.Universe.raise_t Prims.unit -> Steel.Effect.Common.vprop) ->
    _:
      Steel.ST.GenElim1.Base.curried_function_type ty
        (_: FStar.Universe.raise_t Prims.unit -> Prims.prop)
  -> Steel.ST.GenElim1.Base.gen_elim_tele
Prims.list Steel.ST.GenElim1.Base.curried_function_type FStar.Universe.raise_t Prims.unit Steel.Effect.Common.vprop Prims.prop Steel.ST.GenElim1.Base.gen_elim_tele Prims.Nil Steel.ST.GenElim1.Base.TRet FStar.Universe.raise_val Prims.Cons Steel.ST.GenElim1.Base.TExists Steel.ST.GenElim1.Base.gen_elim_nondep_sem
let rec gen_elim_nondep_sem (ty: list (Type u#a))
    : Tot
    (
          curried_function_type ty (U.raise_t u#_ u#(max 2 a) unit -> vprop) ->
          curried_function_type ty (U.raise_t u#_ u#(max 2 a) unit -> prop)
        -> Tot (gen_elim_tele u#a)) =
  
match
  ty
    as ty'
      returns

            curried_function_type ty' (U.raise_t u#_ u#(max 2 a) unit -> vprop) ->
            curried_function_type ty' (U.raise_t u#_ u#(max 2 a) unit -> prop)
          -> Tot gen_elim_tele
with
| [] -> fun q post -> TRet (q (U.raise_val ())) (post (U.raise_val ()))
| t :: tq -> fun q post -> TExists t (fun x -> gen_elim_nondep_sem tq (q x) (post x))