val compute_uncurry:
    ret_type: Type u#a ->
    def: ret_type ->
    ty: list Type0 ->
    curried_function_type ty ret_type ->
    compute_gen_elim_nondep_a' ty
  -> ret_type
let compute_uncurry (ret_type: Type u#a) (def: ret_type) (ty: list Type0) : curried_function_type ty ret_type -> compute_gen_elim_nondep_a' ty -> ret_type =
    match ty as ty' returns (curried_function_type ty' ret_type -> compute_gen_elim_nondep_a' ty' -> ret_type) with
    | [] -> fun q _ -> q
    | [t1] -> fun q -> q
    | [t1; t2] -> fun q x -> q (fstp x) (sndp x)
    | [t1; t2; t3] -> fun q x -> q x._1 x._2 x._3
    | [t1; t2; t3; t4] -> fun q x -> q x._1 x._2 x._3 x._4
    | [t1; t2; t3; t4; t5] -> fun q x -> q x._1 x._2 x._3 x._4 x._5
    | [t1; t2; t3; t4; t5; t6] -> fun q x -> q x._1 x._2 x._3 x._4 x._5 x._6
    | [t1; t2; t3; t4; t5; t6; t7] -> fun q x -> q x._1 x._2 x._3 x._4 x._5 x._6 x._7
    | [t1; t2; t3; t4; t5; t6; t7; t8] -> fun q x -> q x._1 x._2 x._3 x._4 x._5 x._6 x._7 x._8
    | [t1; t2; t3; t4; t5; t6; t7; t8; t9] -> fun q x -> q x._1 x._2 x._3 x._4 x._5 x._6 x._7 x._8 x._9
    | [t1; t2; t3; t4; t5; t6; t7; t8; t9; t10] -> fun q x -> q x._1 x._2 x._3 x._4 x._5 x._6 x._7 x._8 x._9 x._10
    | [t1; t2; t3; t4; t5; t6; t7; t8; t9; t10; t11] -> fun q x -> q x._1 x._2 x._3 x._4 x._5 x._6 x._7 x._8 x._9 x._10 x._11
    | [t1; t2; t3; t4; t5; t6; t7; t8; t9; t10; t11; t12] -> fun q x -> q x._1 x._2 x._3 x._4 x._5 x._6 x._7 x._8 x._9 x._10 x._11 x._12
    | [t1; t2; t3; t4; t5; t6; t7; t8; t9; t10; t11; t12; t13] -> fun q x -> q x._1 x._2 x._3 x._4 x._5 x._6 x._7 x._8 x._9 x._10 x._11 x._12 x._13
    | [t1; t2; t3; t4; t5; t6; t7; t8; t9; t10; t11; t12; t13; t14] -> fun q x -> q x._1 x._2 x._3 x._4 x._5 x._6 x._7 x._8 x._9 x._10 x._11 x._12 x._13 x._14
    | _ -> fun _ _ -> def
val compute_uncurry:
    ret_type: Type u#a ->
    def: ret_type ->
    ty: list Type0 ->
    curried_function_type ty ret_type ->
    compute_gen_elim_nondep_a' ty
  -> ret_type
let compute_uncurry (ret_type: Type u#a) (def: ret_type) (ty: list Type0)
    :  curried_function_type ty ret_type -> compute_gen_elim_nondep_a' ty -> ret_type =
match
  ty
    as ty'
      returns (curried_function_type ty' ret_type -> compute_gen_elim_nondep_a' ty' -> ret_type)
with
| [] -> fun q _ -> q
| [t1] -> fun q -> q
| [t1 ; t2] -> fun q x -> q (fstp x) (sndp x)
| [t1 ; t2 ; t3] -> fun q x -> q x._1 x._2 x._3
| [t1 ; t2 ; t3 ; t4] -> fun q x -> q x._1 x._2 x._3 x._4
| [t1 ; t2 ; t3 ; t4 ; t5] -> fun q x -> q x._1 x._2 x._3 x._4 x._5
| [t1 ; t2 ; t3 ; t4 ; t5 ; t6] -> fun q x -> q x._1 x._2 x._3 x._4 x._5 x._6
| [t1 ; t2 ; t3 ; t4 ; t5 ; t6 ; t7] -> fun q x -> q x._1 x._2 x._3 x._4 x._5 x._6 x._7
| [t1 ; t2 ; t3 ; t4 ; t5 ; t6 ; t7 ; t8] -> fun q x -> q x._1 x._2 x._3 x._4 x._5 x._6 x._7 x._8
| [t1 ; t2 ; t3 ; t4 ; t5 ; t6 ; t7 ; t8 ; t9] ->
  fun q x -> q x._1 x._2 x._3 x._4 x._5 x._6 x._7 x._8 x._9
| [t1 ; t2 ; t3 ; t4 ; t5 ; t6 ; t7 ; t8 ; t9 ; t10] ->
  fun q x -> q x._1 x._2 x._3 x._4 x._5 x._6 x._7 x._8 x._9 x._10
| [t1 ; t2 ; t3 ; t4 ; t5 ; t6 ; t7 ; t8 ; t9 ; t10 ; t11] ->
  fun q x -> q x._1 x._2 x._3 x._4 x._5 x._6 x._7 x._8 x._9 x._10 x._11
| [t1 ; t2 ; t3 ; t4 ; t5 ; t6 ; t7 ; t8 ; t9 ; t10 ; t11 ; t12] ->
  fun q x -> q x._1 x._2 x._3 x._4 x._5 x._6 x._7 x._8 x._9 x._10 x._11 x._12
| [t1 ; t2 ; t3 ; t4 ; t5 ; t6 ; t7 ; t8 ; t9 ; t10 ; t11 ; t12 ; t13] ->
  fun q x -> q x._1 x._2 x._3 x._4 x._5 x._6 x._7 x._8 x._9 x._10 x._11 x._12 x._13
| [t1 ; t2 ; t3 ; t4 ; t5 ; t6 ; t7 ; t8 ; t9 ; t10 ; t11 ; t12 ; t13 ; t14] ->
  fun q x -> q x._1 x._2 x._3 x._4 x._5 x._6 x._7 x._8 x._9 x._10 x._11 x._12 x._13 x._14
| _ -> fun _ _ -> def
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
Prims.list Steel.ST.GenElim.Base.curried_function_type Steel.ST.GenElim.Base.compute_gen_elim_nondep_a' Prims.Nil Prims.Cons Steel.ST.GenElim.Base.fstp Steel.ST.GenElim.Base.sndp FStar.Pervasives.Native.__proj__Mktuple3__item___1 FStar.Pervasives.Native.__proj__Mktuple3__item___2 FStar.Pervasives.Native.__proj__Mktuple3__item___3 FStar.Pervasives.Native.__proj__Mktuple4__item___1 FStar.Pervasives.Native.__proj__Mktuple4__item___2 FStar.Pervasives.Native.__proj__Mktuple4__item___3 FStar.Pervasives.Native.__proj__Mktuple4__item___4 FStar.Pervasives.Native.__proj__Mktuple5__item___1 FStar.Pervasives.Native.__proj__Mktuple5__item___2 FStar.Pervasives.Native.__proj__Mktuple5__item___3 FStar.Pervasives.Native.__proj__Mktuple5__item___4 FStar.Pervasives.Native.__proj__Mktuple5__item___5 FStar.Pervasives.Native.__proj__Mktuple6__item___1 FStar.Pervasives.Native.__proj__Mktuple6__item___2 FStar.Pervasives.Native.__proj__Mktuple6__item___3 FStar.Pervasives.Native.__proj__Mktuple6__item___4 FStar.Pervasives.Native.__proj__Mktuple6__item___5 FStar.Pervasives.Native.__proj__Mktuple6__item___6 FStar.Pervasives.Native.__proj__Mktuple7__item___1 FStar.Pervasives.Native.__proj__Mktuple7__item___2 FStar.Pervasives.Native.__proj__Mktuple7__item___3 FStar.Pervasives.Native.__proj__Mktuple7__item___4 FStar.Pervasives.Native.__proj__Mktuple7__item___5 FStar.Pervasives.Native.__proj__Mktuple7__item___6 FStar.Pervasives.Native.__proj__Mktuple7__item___7 FStar.Pervasives.Native.__proj__Mktuple8__item___1 FStar.Pervasives.Native.__proj__Mktuple8__item___2 FStar.Pervasives.Native.__proj__Mktuple8__item___3 FStar.Pervasives.Native.__proj__Mktuple8__item___4 FStar.Pervasives.Native.__proj__Mktuple8__item___5 FStar.Pervasives.Native.__proj__Mktuple8__item___6 FStar.Pervasives.Native.__proj__Mktuple8__item___7 FStar.Pervasives.Native.__proj__Mktuple8__item___8 FStar.Pervasives.Native.__proj__Mktuple9__item___1 FStar.Pervasives.Native.__proj__Mktuple9__item___2 FStar.Pervasives.Native.__proj__Mktuple9__item___3 FStar.Pervasives.Native.__proj__Mktuple9__item___4 FStar.Pervasives.Native.__proj__Mktuple9__item___5 FStar.Pervasives.Native.__proj__Mktuple9__item___6 FStar.Pervasives.Native.__proj__Mktuple9__item___7 FStar.Pervasives.Native.__proj__Mktuple9__item___8 FStar.Pervasives.Native.__proj__Mktuple9__item___9 FStar.Pervasives.Native.__proj__Mktuple10__item___1 FStar.Pervasives.Native.__proj__Mktuple10__item___2 FStar.Pervasives.Native.__proj__Mktuple10__item___3 FStar.Pervasives.Native.__proj__Mktuple10__item___4 FStar.Pervasives.Native.__proj__Mktuple10__item___5 FStar.Pervasives.Native.__proj__Mktuple10__item___6 FStar.Pervasives.Native.__proj__Mktuple10__item___7 FStar.Pervasives.Native.__proj__Mktuple10__item___8 FStar.Pervasives.Native.__proj__Mktuple10__item___9 FStar.Pervasives.Native.__proj__Mktuple10__item___10 FStar.Pervasives.Native.__proj__Mktuple11__item___1 FStar.Pervasives.Native.__proj__Mktuple11__item___2 FStar.Pervasives.Native.__proj__Mktuple11__item___3 FStar.Pervasives.Native.__proj__Mktuple11__item___4 FStar.Pervasives.Native.__proj__Mktuple11__item___5 FStar.Pervasives.Native.__proj__Mktuple11__item___6 FStar.Pervasives.Native.__proj__Mktuple11__item___7 FStar.Pervasives.Native.__proj__Mktuple11__item___8 FStar.Pervasives.Native.__proj__Mktuple11__item___9 FStar.Pervasives.Native.__proj__Mktuple11__item___10 FStar.Pervasives.Native.__proj__Mktuple11__item___11 FStar.Pervasives.Native.__proj__Mktuple12__item___1 FStar.Pervasives.Native.__proj__Mktuple12__item___2 FStar.Pervasives.Native.__proj__Mktuple12__item___3 FStar.Pervasives.Native.__proj__Mktuple12__item___4 FStar.Pervasives.Native.__proj__Mktuple12__item___5 FStar.Pervasives.Native.__proj__Mktuple12__item___6 FStar.Pervasives.Native.__proj__Mktuple12__item___7 FStar.Pervasives.Native.__proj__Mktuple12__item___8 FStar.Pervasives.Native.__proj__Mktuple12__item___9 FStar.Pervasives.Native.__proj__Mktuple12__item___10 FStar.Pervasives.Native.__proj__Mktuple12__item___11 FStar.Pervasives.Native.__proj__Mktuple12__item___12 FStar.Pervasives.Native.__proj__Mktuple13__item___1 FStar.Pervasives.Native.__proj__Mktuple13__item___2 FStar.Pervasives.Native.__proj__Mktuple13__item___3 FStar.Pervasives.Native.__proj__Mktuple13__item___4 FStar.Pervasives.Native.__proj__Mktuple13__item___5 FStar.Pervasives.Native.__proj__Mktuple13__item___6 FStar.Pervasives.Native.__proj__Mktuple13__item___7 FStar.Pervasives.Native.__proj__Mktuple13__item___8 FStar.Pervasives.Native.__proj__Mktuple13__item___9 FStar.Pervasives.Native.__proj__Mktuple13__item___10 FStar.Pervasives.Native.__proj__Mktuple13__item___11 FStar.Pervasives.Native.__proj__Mktuple13__item___12 FStar.Pervasives.Native.__proj__Mktuple13__item___13 FStar.Pervasives.Native.__proj__Mktuple14__item___1 FStar.Pervasives.Native.__proj__Mktuple14__item___2 FStar.Pervasives.Native.__proj__Mktuple14__item___3 FStar.Pervasives.Native.__proj__Mktuple14__item___4 FStar.Pervasives.Native.__proj__Mktuple14__item___5 FStar.Pervasives.Native.__proj__Mktuple14__item___6 FStar.Pervasives.Native.__proj__Mktuple14__item___7 FStar.Pervasives.Native.__proj__Mktuple14__item___8 FStar.Pervasives.Native.__proj__Mktuple14__item___9 FStar.Pervasives.Native.__proj__Mktuple14__item___10 FStar.Pervasives.Native.__proj__Mktuple14__item___11 FStar.Pervasives.Native.__proj__Mktuple14__item___12 FStar.Pervasives.Native.__proj__Mktuple14__item___13 FStar.Pervasives.Native.__proj__Mktuple14__item___14
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)
: 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))

[@@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')
  | GEExistsNoAbs #a p -> p
  | GEExistsUnit #a p -> fun v -> compute_gen_unit_elim_q (p v)
  | GEExists #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')
  | GEExistsNoAbs #a p -> fun _ -> True
  | GEExistsUnit #a p -> fun v -> compute_gen_unit_elim_post (p v)
  | GEExists #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 =
  | TRet: vprop -> prop -> gen_elim_tele
  | TExists: (ty: Type u#0) -> (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 =
  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)
  | GEExistsNoAbs #ty body -> TExists ty (fun x -> TRet (body x) True)
  | GEExistsUnit #ty body -> TExists ty (fun x -> TRet (compute_gen_unit_elim_q (body x)) (compute_gen_unit_elim_post (body x)))
  | GEExists #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 =
| GENonDep: (ty: list Type0) -> curried_function_type ty vprop -> curried_function_type ty prop -> gen_elim_nondep_t
| GEDep

[@@gen_elim_reduce]
let mk_gen_elim_nondep
  (ty: list Type0)
  (tvprop: Type)
  (q: tvprop)
  (tprop: Type)
  (post: tprop)
: Pure gen_elim_nondep_t
  (requires (
    tvprop == curried_function_type ty vprop /\
    tprop == curried_function_type ty prop
  ))
  (ensures (fun _ -> True))
= GENonDep ty q post

[@@gen_elim_reduce]
let mk_gen_elim_nondep_by_tac
  (ty: list Type0)
  (tvprop: Type)
  (q: tvprop)
  (tprop: Type)
  (post: tprop)
: Pure gen_elim_nondep_t
  (requires (
    T.with_tactic (fun _ -> T.norm [delta_attr [(`%gen_elim_reduce)]; iota; zeta]) (tvprop == curried_function_type ty vprop) /\
    T.with_tactic (fun _ -> T.norm [delta_attr [(`%gen_elim_reduce)]; iota; zeta]) (tprop == curried_function_type ty prop)
  ))
  (ensures (fun _ -> True))
= GENonDep ty q post

[@@gen_elim_reduce]
let rec gen_elim_nondep_sem (ty: list Type0) : Tot (curried_function_type ty vprop -> curried_function_type ty prop -> Tot gen_elim_tele) =
  match ty as ty' returns curried_function_type ty' vprop -> curried_function_type ty' prop -> Tot gen_elim_tele with
  | [] -> fun q post -> TRet q post
  | t :: tq -> fun q post -> TExists t (fun x -> gen_elim_nondep_sem tq (q x) (post x))

[@@gen_elim_reduce; noextract_to "Plugin"]
let check_gen_elim_nondep_sem (i: gen_elim_i) (nd: gen_elim_nondep_t) : Tot prop =
  match nd with
  | GENonDep ty q post -> compute_gen_elim_tele i == gen_elim_nondep_sem ty q post
  | GEDep -> True

[@@gen_elim_reduce; noextract_to "Plugin"]
let compute_gen_elim_nondep_a' (ty: list Type0) : Tot Type0 =
    match ty with
    | [] -> unit
    | [t1] -> t1
    | [t1; t2] -> tuple2 t1 t2
    | [t1; t2; t3] -> tuple3 t1 t2 t3
    | [t1; t2; t3; t4] -> tuple4 t1 t2 t3 t4
    | [t1; t2; t3; t4; t5] -> tuple5 t1 t2 t3 t4 t5
    | [t1; t2; t3; t4; t5; t6] -> tuple6 t1 t2 t3 t4 t5 t6
    | [t1; t2; t3; t4; t5; t6; t7] -> tuple7 t1 t2 t3 t4 t5 t6 t7
    | [t1; t2; t3; t4; t5; t6; t7; t8] -> tuple8 t1 t2 t3 t4 t5 t6 t7 t8
    | [t1; t2; t3; t4; t5; t6; t7; t8; t9] -> tuple9 t1 t2 t3 t4 t5 t6 t7 t8 t9
    | [t1; t2; t3; t4; t5; t6; t7; t8; t9; t10] -> tuple10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10
    | [t1; t2; t3; t4; t5; t6; t7; t8; t9; t10; t11] -> tuple11 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11
    | [t1; t2; t3; t4; t5; t6; t7; t8; t9; t10; t11; t12] -> tuple12 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12
    | [t1; t2; t3; t4; t5; t6; t7; t8; t9; t10; t11; t12; t13] -> tuple13 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13
    | [t1; t2; t3; t4; t5; t6; t7; t8; t9; t10; t11; t12; t13; t14] -> tuple14 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14
    | _ -> unit // unsupported

[@@gen_elim_reduce; noextract_to "Plugin"]
let compute_gen_elim_nondep_a (i0: gen_elim_i) (i: gen_elim_nondep_t) : Tot Type0 =
  match i with
  | GENonDep ty q post -> compute_gen_elim_nondep_a' ty
  | GEDep -> compute_gen_elim_a i0

[@@gen_elim_reduce; noextract_to "Plugin"]
val compute_uncurry:
    ret_type: Type u#a ->
    def: ret_type ->
    ty: list Type0 ->
    curried_function_type ty ret_type ->
    compute_gen_elim_nondep_a' ty
  -> ret_type

    ret_type: Type ->
    def: ret_type ->
    ty: Prims.list Type0 ->
    _: Steel.ST.GenElim.Base.curried_function_type ty ret_type ->
    _: Steel.ST.GenElim.Base.compute_gen_elim_nondep_a' ty
  -> ret_type