val unzip (#a #b: _) (l: list (a & b)) : Tot (list a & list b)
let rec unzip #a #b (l : list (a & b)) : Tot (list a & list b) =
  match l with
  | [] -> ([],[])
  | (hd1,hd2)::tl ->
       let (tl1,tl2) = unzip tl in
       (hd1::tl1,hd2::tl2)
val unzip (#a #b: _) (l: list (a & b)) : Tot (list a & list b)
let rec unzip #a #b (l: list (a & b)) : Tot (list a & list b) =
match l with
| [] -> ([], [])
| (hd1, hd2) :: tl ->
  let tl1, tl2 = unzip tl in
  (hd1 :: tl1, hd2 :: tl2)
FStar.InteractiveHelpers.Base.fst.checked
prims.fst.checked FStar.Tactics.Util.fst.checked FStar.Tactics.fst.checked FStar.Sealed.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Order.fst.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.List.fst.checked
FStar.InteractiveHelpers.Base.fst
Prims.list FStar.Pervasives.Native.tuple2 FStar.Pervasives.Native.Mktuple2 Prims.Nil Prims.Cons FStar.InteractiveHelpers.Base.unzip
module FStar.InteractiveHelpers.Base

open FStar.List
open FStar.Tactics
open FStar.Mul

#push-options "--z3rlimit 15 --fuel 0 --ifuel 1"

(*** Utilities *)
val bv_eq : bv -> bv -> Tot bool
let bv_eq (bv1 bv2 : bv) =
  let bvv1 = inspect_bv bv1 in
  let bvv2 = inspect_bv bv2 in
  (* We don't check for type equality: the fact that no two different binders
   * have the same name and index is an invariant which must be enforced -
   * and actually we could limit ourselves to checking the index *)
  bvv1.bv_index = bvv2.bv_index

val fv_eq : fv -> fv -> Tot bool
let fv_eq fv1 fv2 =
  let n1 = inspect_fv fv1 in
  let n2 = inspect_fv fv2 in
  n1 = n2

// TODO: use everywhere
val fv_eq_name : fv -> name -> Tot bool
let fv_eq_name fv n =
  let fvn = inspect_fv fv in
  fvn = n

// TODO: use more
val opt_apply (#a #b : Type) (f : a -> Tot b) (x : option a) : Tot (option b)
let opt_apply #a #b f x =
  match x with
  | None -> None
  | Some x' -> Some (f x')

val opt_tapply (#a #b : Type) (f : a -> Tac b) (x : option a) : Tac (option b)
let opt_tapply #a #b f x =
  match x with
  | None -> None
  | Some x' -> Some (f x')

val option_to_string : (#a : Type) -> (a -> Tac string) -> option a -> Tac string
let option_to_string #a f x =
  match x with
  | None -> "None"
  | Some x' -> "Some (" ^ f x' ^ ")"


let opt_cons (#a : Type) (opt_x : option a) (ls : list a) : Tot (list a) =
  match opt_x with
  | Some x -> x :: ls
  | None -> ls

val list_to_string : #a : Type -> (a -> Tac string) -> list a -> Tac string
let list_to_string #a f ls =
  (Tactics.Util.fold_left (fun s x -> s ^ " (" ^ f x ^ ");") "[" ls) ^ "]"


/// Apply a term to a list of parameters, normalize the result to make sure
/// all the abstractions are simplified
val mk_app_norm : env -> term -> list term -> Tac term
let mk_app_norm e t params =
  let t1 = mk_e_app t params in
  let t2 = norm_term_env e [] t1 in
  t2

val opt_mk_app_norm : env -> option term -> list term -> Tac (option term)
let opt_mk_app_norm e opt_t params =
  opt_tapply (fun t -> mk_app_norm e t params) opt_t

// TODO: remove
val unzip (#a #b: _) (l: list (a & b)) : Tot (list a & list b)
l: Prims.list (a * b) -> Prims.list a * Prims.list b