val close_binders (bs: list (var & typ)) (t: term) : term
let close_binders (bs:list (var & typ)) (t:term) : term =
  let r = L.fold_right (fun (x, _) (n, t) ->
    let ss = [ ND x 0 ] in
    n + 1,
    subst_term t (shift_subst_n n ss)
  ) bs (0, t) in
  snd r
val close_binders (bs: list (var & typ)) (t: term) : term
let close_binders (bs: list (var & typ)) (t: term) : term =
let r =
  L.fold_right (fun (x, _) (n, t) ->
        let ss = [ND x 0] in
        n + 1, subst_term t (shift_subst_n n ss))
    bs
    (0, t)
in
snd r
Pulse.Checker.AssertWithBinders.fst.checked
Pulse.Typing.Env.fsti.checked Pulse.Typing.Combinators.fsti.checked Pulse.Typing.fst.checked Pulse.Syntax.Printer.fsti.checked Pulse.Syntax.Naming.fsti.checked Pulse.Syntax.fst.checked Pulse.RuntimeUtils.fsti.checked Pulse.Elaborate.Pure.fst.checked Pulse.Checker.Pure.fsti.checked Pulse.Checker.Prover.Substs.fsti.checked Pulse.Checker.Prover.fsti.checked Pulse.Checker.Base.fsti.checked prims.fst.checked FStar.Tactics.Visit.fst.checked FStar.Tactics.V2.fst.checked FStar.String.fsti.checked FStar.Set.fsti.checked FStar.Reflection.V2.TermEq.fst.checked FStar.Reflection.V2.fst.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Pulse.Checker.AssertWithBinders.fst
Prims.list FStar.Pervasives.Native.tuple2 Pulse.Syntax.Base.var Pulse.Syntax.Base.typ Pulse.Syntax.Base.term FStar.Pervasives.Native.snd Prims.int Prims.b2t Prims.op_GreaterThanOrEqual FStar.List.Tot.Base.fold_right FStar.Pervasives.Native.Mktuple2 Prims.op_Addition Pulse.Syntax.Naming.subst_term Pulse.Syntax.Naming.shift_subst_n Pulse.Syntax.Naming.subst_elt Prims.Cons Pulse.Syntax.Naming.ND Prims.Nil
module Pulse.Checker.AssertWithBinders


open Pulse.Syntax
open Pulse.Typing
open Pulse.Checker.Base
open Pulse.Elaborate.Pure
open Pulse.Typing.Env

module L = FStar.List.Tot
module T = FStar.Tactics.V2
module R = FStar.Reflection.V2
module PC = Pulse.Checker.Pure
module P = Pulse.Syntax.Printer
module N = Pulse.Syntax.Naming
module PS = Pulse.Checker.Prover.Substs
module Prover = Pulse.Checker.Prover

module RU = Pulse.RuntimeUtils

let is_host_term (t:R.term) = not (R.Tv_Unknown? (R.inspect_ln t))

let debug_log = Pulse.Typing.debug_log "with_binders"

let option_must (f:option 'a) (msg:string) : T.Tac 'a =
  match f with
  | Some x -> x
  | None -> T.fail msg

let rec refl_abs_binders (t:R.term) (acc:list binder) : T.Tac (list binder) =
  let open R in
  match inspect_ln t with
  | Tv_Abs b body ->
    let {sort; ppname} = R.inspect_binder b in
    let sort = option_must (readback_ty sort)
      (Printf.sprintf "Failed to readback elaborated binder sort %s in refl_abs_binders"
         (T.term_to_string sort)) in
    refl_abs_binders body
     ({ binder_ty = sort; binder_ppname = mk_ppname ppname (RU.range_of_term t) }::acc)
  | _ -> L.rev acc  

let infer_binder_types (g:env) (bs:list binder) (v:vprop)
  : T.Tac (list binder) =
  match bs with
  | [] -> []
  | _ ->
    let tv = elab_term v in
    if not (is_host_term tv)
    then fail g (Some v.range)
           (Printf.sprintf "assert.infer_binder_types: elaborated %s to %s, which failed the host term check"
              (P.term_to_string v) (T.term_to_string tv));
    let as_binder (b:binder) : R.binder =
      let open R in
      let bv : binder_view = 
        { sort = elab_term b.binder_ty;
          ppname = b.binder_ppname.name;
          qual = Q_Explicit;
          attrs = [] } in
      pack_binder bv
    in
    let abstraction = 
      L.fold_right 
        (fun b (tv:host_term) -> 
         let b = as_binder b in
         R.pack_ln (R.Tv_Abs b tv))
        bs
        tv
    in
    let inst_abstraction, _ = PC.instantiate_term_implicits g (tm_fstar abstraction v.range) in
    match inst_abstraction.t with
    | Tm_FStar t -> refl_abs_binders t []
    | _ -> T.fail "Impossible: instantiated abstraction is not embedded F* term, please file a bug-report"

let rec open_binders (g:env) (bs:list binder) (uvs:env { disjoint uvs g }) (v:term) (body:st_term)
  : T.Tac (uvs:env { disjoint uvs g } & term & st_term) =

  match bs with
  | [] -> (| uvs, v, body |)
  | b::bs ->
    // these binders are only lax checked so far
    let _ = PC.check_universe (push_env g uvs) b.binder_ty in
    let x = fresh (push_env g uvs) in
    let ss = [ DT 0 (tm_var {nm_index=x;nm_ppname=b.binder_ppname}) ] in
    let bs = L.mapi (fun i b ->
      assume (i >= 0);
      subst_binder b (shift_subst_n i ss)) bs in
    let v = subst_term v (shift_subst_n (L.length bs) ss) in
    let body = subst_st_term body (shift_subst_n (L.length bs) ss) in
    open_binders g bs (push_binding uvs x b.binder_ppname b.binder_ty) v body
val close_binders (bs: list (var & typ)) (t: term) : term
bs: Prims.list (Pulse.Syntax.Base.var * Pulse.Syntax.Base.typ) -> t: Pulse.Syntax.Base.term
  -> Pulse.Syntax.Base.term