val mk_bind (g:env)
            (pre:term)
            (e1:st_term)
            (e2:st_term)
            (c1:comp_st)
            (c2:comp_st)
            (px:nvar { ~ (Set.mem (snd px) (dom g)) })
            (d_e1:st_typing g e1 c1)
            (d_c1res:tot_typing g (comp_res c1) (tm_type (comp_u c1)))
            (d_e2:st_typing (push_binding g (snd px) (fst px) (comp_res c1)) (open_st_term_nv e2 px) c2)
            (res_typing:universe_of g (comp_res c2) (comp_u c2))
            (post_typing:tot_typing (push_binding g (snd px) (fst px) (comp_res c2))
                                     (open_term_nv (comp_post c2) px)
                                     tm_vprop)
  : T.TacH (t:st_term &
            c:comp_st { st_comp_of_comp c == st_comp_with_pre (st_comp_of_comp c2) pre } &
            st_typing g t c)
           (requires fun _ ->
              let _, x = px in
              comp_pre c1 == pre /\
              None? (lookup g x) /\
              (~(x `Set.mem` freevars_st e2)) /\
              open_term (comp_post c1) x == comp_pre c2 /\
              (~ (x `Set.mem` freevars (comp_post c2))))
           (ensures fun _ _ -> True)
let rec mk_bind (g:env)
                (pre:term)
                (e1:st_term)
                (e2:st_term)
                (c1:comp_st)
                (c2:comp_st)
                (px:nvar { ~ (Set.mem (snd px) (dom g)) })
                (d_e1:st_typing g e1 c1)
                (d_c1res:tot_typing g (comp_res c1) (tm_type (comp_u c1)))
                (d_e2:st_typing (push_binding g (snd px) (fst px) (comp_res c1)) (open_st_term_nv e2 px) c2)
                (res_typing:universe_of g (comp_res c2) (comp_u c2))
                (post_typing:tot_typing (push_binding g (snd px) (fst px) (comp_res c2))
                                        (open_term_nv (comp_post c2) px)
                                        tm_vprop)
  : T.TacH (t:st_term &
            c:comp_st { st_comp_of_comp c == st_comp_with_pre (st_comp_of_comp c2) pre } &
            st_typing g t c)
           (requires fun _ ->
              let _, x = px in
              comp_pre c1 == pre /\
              None? (lookup g x) /\
              (~(x `Set.mem` freevars_st e2)) /\
              open_term (comp_post c1) x == comp_pre c2 /\
              (~ (x `Set.mem` freevars (comp_post c2))))
           (ensures fun _ _ -> True) =
  let _, x = px in
  let b = nvar_as_binder px (comp_res c1) in
  match c1, c2 with
  | C_ST _, C_ST _ ->
    let bc = Bind_comp g x c1 c2 res_typing x post_typing in
    (| _, _, T_Bind _ e1 e2 _ _ b _ _ d_e1 d_c1res d_e2 bc |)
  | C_STGhost inames1 _, C_STGhost inames2 _ ->
    if eq_tm inames1 inames2
    then begin
      let bc = Bind_comp g x c1 c2 res_typing x post_typing in
      (| _, _, T_Bind _ e1 e2 _ _ b _ _ d_e1 d_c1res d_e2 bc |)
    end
    else fail g None "Cannot compose two stghost computations with different opened invariants"
  | C_STAtomic inames _, C_ST _ ->
    if eq_tm inames tm_emp_inames
    then begin
      let c1lifted = C_ST (st_comp_of_comp c1) in
      let d_e1 : st_typing g e1 c1lifted =
        T_Lift _ _ _ c1lifted d_e1 (Lift_STAtomic_ST _ c1) in
      let bc = Bind_comp g x c1lifted c2 res_typing x post_typing in
      (| _, _, T_Bind _ e1 e2 _ _ b _ _ d_e1 d_c1res d_e2 bc |)
    end
    else fail g None "Cannot compose atomic with non-emp opened invariants with stt"
  | C_STGhost inames1 _, C_STAtomic inames2 _ ->
    if eq_tm inames1 inames2
    then begin
      let w = get_non_informative_witness g (comp_u c1) (comp_res c1) in
      let bc = Bind_comp_ghost_l g x c1 c2 w res_typing x post_typing in
      (| _, _, T_Bind _ e1 e2 _ _ b _ _ d_e1 d_c1res d_e2 bc |)
    end
    else fail g None "Cannot compose ghost and atomic with different opened invariants"
  | C_STAtomic inames1 _, C_STGhost inames2 _ ->
    if eq_tm inames1 inames2
    then begin
      let w = get_non_informative_witness g (comp_u c2) (comp_res c2) in
      let bc = Bind_comp_ghost_r g x c1 c2 w res_typing x post_typing in
      (| _, _, T_Bind _ e1 e2 _ _ b _ _ d_e1 d_c1res d_e2 bc |)
    end
    else fail g None "Cannot compose atomic and ghost with different opened invariants"
  | C_ST _, C_STAtomic inames _ ->
    if eq_tm inames tm_emp_inames
    then begin
      let c2lifted = C_ST (st_comp_of_comp c2) in
      let g' = push_binding g x (fst px) (comp_res c1) in
      let d_e2 : st_typing g' (open_st_term_nv e2 px) c2lifted =
        T_Lift _ _ _ c2lifted d_e2 (Lift_STAtomic_ST _ c2) in
      let bc = Bind_comp g x c1 c2lifted res_typing x post_typing in
      (| _, _, T_Bind _ e1 e2 _ _ b _ _ d_e1 d_c1res d_e2 bc |)
    end
    else fail g None "Cannot compose stt with atomic with non-emp opened invariants"
  | C_STGhost inames _, C_ST _ ->
    if eq_tm inames tm_emp_inames
    then begin
      let w = get_non_informative_witness g (comp_u c1) (comp_res c1) in
      let c1lifted = C_STAtomic inames (st_comp_of_comp c1) in
      let d_e1 : st_typing g e1 c1lifted =
        T_Lift _ _ _ c1lifted d_e1 (Lift_STGhost_STAtomic g c1 w) in
      mk_bind g pre e1 e2 c1lifted c2 px d_e1 d_c1res d_e2 res_typing post_typing
    end
    else fail g None "Cannot compose ghost with stt with non-emp opened invariants"
  | C_ST _, C_STGhost inames _ ->
    if eq_tm inames tm_emp_inames
    then begin
      let g' = push_binding g x (fst px) (comp_res c1) in
      let w = get_non_informative_witness g' (comp_u c2) (comp_res c2) in
      let c2lifted = C_STAtomic inames (st_comp_of_comp c2) in
      let d_e2 : st_typing g' (open_st_term_nv e2 px) c2lifted =
        T_Lift _ _ _ c2lifted d_e2 (Lift_STGhost_STAtomic g' c2 w) in
      let (| t, c, d |) = mk_bind g pre e1 e2 c1 c2lifted px d_e1 d_c1res d_e2 res_typing post_typing in
      (| t, c, d |)
    end
    else fail g None "Cannot compose stt with ghost with non-emp opened invariants"
  | C_STAtomic inames _, C_STAtomic _ _ ->
    if eq_tm inames tm_emp_inames
    then begin
      let c1lifted = C_ST (st_comp_of_comp c1) in
      let d_e1 : st_typing g e1 c1lifted =
        T_Lift _ _ _ c1lifted d_e1 (Lift_STAtomic_ST _ c1) in
      mk_bind g pre e1 e2 c1lifted c2 px d_e1 d_c1res d_e2 res_typing post_typing
    end
    else fail g None "Cannot compose statomics with non-emp opened invariants"
  | _, _ -> fail g None "bind either not implemented (e.g. ghost) or not possible"
val mk_bind (g:env)
            (pre:term)
            (e1:st_term)
            (e2:st_term)
            (c1:comp_st)
            (c2:comp_st)
            (px:nvar { ~ (Set.mem (snd px) (dom g)) })
            (d_e1:st_typing g e1 c1)
            (d_c1res:tot_typing g (comp_res c1) (tm_type (comp_u c1)))
            (d_e2:st_typing (push_binding g (snd px) (fst px) (comp_res c1)) (open_st_term_nv e2 px) c2)
            (res_typing:universe_of g (comp_res c2) (comp_u c2))
            (post_typing:tot_typing (push_binding g (snd px) (fst px) (comp_res c2))
                                     (open_term_nv (comp_post c2) px)
                                     tm_vprop)
  : T.TacH (t:st_term &
            c:comp_st { st_comp_of_comp c == st_comp_with_pre (st_comp_of_comp c2) pre } &
            st_typing g t c)
           (requires fun _ ->
              let _, x = px in
              comp_pre c1 == pre /\
              None? (lookup g x) /\
              (~(x `Set.mem` freevars_st e2)) /\
              open_term (comp_post c1) x == comp_pre c2 /\
              (~ (x `Set.mem` freevars (comp_post c2))))
           (ensures fun _ _ -> True)
let rec mk_bind
      (g: env)
      (pre: term)
      (e1 e2: st_term)
      (c1 c2: comp_st)
      (px: nvar{~(Set.mem (snd px) (dom g))})
      (d_e1: st_typing g e1 c1)
      (d_c1res: tot_typing g (comp_res c1) (tm_type (comp_u c1)))
      (d_e2: st_typing (push_binding g (snd px) (fst px) (comp_res c1)) (open_st_term_nv e2 px) c2)
      (res_typing: universe_of g (comp_res c2) (comp_u c2))
      (post_typing:
          tot_typing (push_binding g (snd px) (fst px) (comp_res c2))
            (open_term_nv (comp_post c2) px)
            tm_vprop)
    : T.TacH
      (t: st_term &
        c: comp_st{st_comp_of_comp c == st_comp_with_pre (st_comp_of_comp c2) pre} &
        st_typing g t c)
      (requires
        fun _ ->
          let _, x = px in
          comp_pre c1 == pre /\ None? (lookup g x) /\ (~(x `Set.mem` (freevars_st e2))) /\
          open_term (comp_post c1) x == comp_pre c2 /\ (~(x `Set.mem` (freevars (comp_post c2)))))
      (ensures fun _ _ -> True) =
let _, x = px in
let b = nvar_as_binder px (comp_res c1) in
match c1, c2 with
| C_ST _, C_ST _ ->
  let bc = Bind_comp g x c1 c2 res_typing x post_typing in
  (| _, _, T_Bind _ e1 e2 _ _ b _ _ d_e1 d_c1res d_e2 bc |)
| C_STGhost inames1 _, C_STGhost inames2 _ ->
  if eq_tm inames1 inames2
  then
    let bc = Bind_comp g x c1 c2 res_typing x post_typing in
    (| _, _, T_Bind _ e1 e2 _ _ b _ _ d_e1 d_c1res d_e2 bc |)
  else fail g None "Cannot compose two stghost computations with different opened invariants"
| C_STAtomic inames _, C_ST _ ->
  if eq_tm inames tm_emp_inames
  then
    let c1lifted = C_ST (st_comp_of_comp c1) in
    let d_e1:st_typing g e1 c1lifted = T_Lift _ _ _ c1lifted d_e1 (Lift_STAtomic_ST _ c1) in
    let bc = Bind_comp g x c1lifted c2 res_typing x post_typing in
    (| _, _, T_Bind _ e1 e2 _ _ b _ _ d_e1 d_c1res d_e2 bc |)
  else fail g None "Cannot compose atomic with non-emp opened invariants with stt"
| C_STGhost inames1 _, C_STAtomic inames2 _ ->
  if eq_tm inames1 inames2
  then
    let w = get_non_informative_witness g (comp_u c1) (comp_res c1) in
    let bc = Bind_comp_ghost_l g x c1 c2 w res_typing x post_typing in
    (| _, _, T_Bind _ e1 e2 _ _ b _ _ d_e1 d_c1res d_e2 bc |)
  else fail g None "Cannot compose ghost and atomic with different opened invariants"
| C_STAtomic inames1 _, C_STGhost inames2 _ ->
  if eq_tm inames1 inames2
  then
    let w = get_non_informative_witness g (comp_u c2) (comp_res c2) in
    let bc = Bind_comp_ghost_r g x c1 c2 w res_typing x post_typing in
    (| _, _, T_Bind _ e1 e2 _ _ b _ _ d_e1 d_c1res d_e2 bc |)
  else fail g None "Cannot compose atomic and ghost with different opened invariants"
| C_ST _, C_STAtomic inames _ ->
  if eq_tm inames tm_emp_inames
  then
    let c2lifted = C_ST (st_comp_of_comp c2) in
    let g' = push_binding g x (fst px) (comp_res c1) in
    let d_e2:st_typing g' (open_st_term_nv e2 px) c2lifted =
      T_Lift _ _ _ c2lifted d_e2 (Lift_STAtomic_ST _ c2)
    in
    let bc = Bind_comp g x c1 c2lifted res_typing x post_typing in
    (| _, _, T_Bind _ e1 e2 _ _ b _ _ d_e1 d_c1res d_e2 bc |)
  else fail g None "Cannot compose stt with atomic with non-emp opened invariants"
| C_STGhost inames _, C_ST _ ->
  if eq_tm inames tm_emp_inames
  then
    let w = get_non_informative_witness g (comp_u c1) (comp_res c1) in
    let c1lifted = C_STAtomic inames (st_comp_of_comp c1) in
    let d_e1:st_typing g e1 c1lifted = T_Lift _ _ _ c1lifted d_e1 (Lift_STGhost_STAtomic g c1 w) in
    mk_bind g pre e1 e2 c1lifted c2 px d_e1 d_c1res d_e2 res_typing post_typing
  else fail g None "Cannot compose ghost with stt with non-emp opened invariants"
| C_ST _, C_STGhost inames _ ->
  if eq_tm inames tm_emp_inames
  then
    let g' = push_binding g x (fst px) (comp_res c1) in
    let w = get_non_informative_witness g' (comp_u c2) (comp_res c2) in
    let c2lifted = C_STAtomic inames (st_comp_of_comp c2) in
    let d_e2:st_typing g' (open_st_term_nv e2 px) c2lifted =
      T_Lift _ _ _ c2lifted d_e2 (Lift_STGhost_STAtomic g' c2 w)
    in
    let (| t , c , d |) =
      mk_bind g pre e1 e2 c1 c2lifted px d_e1 d_c1res d_e2 res_typing post_typing
    in
    (| t, c, d |)
  else fail g None "Cannot compose stt with ghost with non-emp opened invariants"
| C_STAtomic inames _, C_STAtomic _ _ ->
  if eq_tm inames tm_emp_inames
  then
    let c1lifted = C_ST (st_comp_of_comp c1) in
    let d_e1:st_typing g e1 c1lifted = T_Lift _ _ _ c1lifted d_e1 (Lift_STAtomic_ST _ c1) in
    mk_bind g pre e1 e2 c1lifted c2 px d_e1 d_c1res d_e2 res_typing post_typing
  else fail g None "Cannot compose statomics with non-emp opened invariants"
| _, _ -> fail g None "bind either not implemented (e.g. ghost) or not possible"
Pulse.Typing.Combinators.fst.checked
Pulse.Typing.Metatheory.fsti.checked Pulse.Typing.fst.checked Pulse.Syntax.Printer.fsti.checked Pulse.Syntax.fst.checked Pulse.Checker.Pure.fsti.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Set.fsti.checked FStar.Reflection.V2.fst.checked FStar.Reflection.Typing.fsti.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Pulse.Typing.Combinators.fst
Pulse.Typing.Env.env Pulse.Syntax.Base.term Pulse.Syntax.Base.st_term Pulse.Syntax.Base.comp_st Pulse.Syntax.Base.nvar Prims.l_not Prims.b2t FStar.Set.mem Pulse.Syntax.Base.var FStar.Pervasives.Native.snd Pulse.Syntax.Base.ppname Pulse.Typing.Env.dom Pulse.Typing.st_typing Pulse.Typing.tot_typing Pulse.Syntax.Base.comp_res Pulse.Syntax.Pure.tm_type Pulse.Syntax.Base.comp_u Pulse.Typing.Env.push_binding FStar.Pervasives.Native.fst Pulse.Syntax.Naming.open_st_term_nv Pulse.Typing.universe_of Pulse.Syntax.Naming.open_term_nv Pulse.Syntax.Base.comp_post Pulse.Syntax.Base.tm_vprop FStar.Pervasives.Native.Mktuple2 Pulse.Syntax.Base.comp Pulse.Syntax.Base.st_comp FStar.Pervasives.Mkdtuple3 Prims.eq2 Pulse.Syntax.Base.st_comp_of_comp Pulse.Typing.Combinators.st_comp_with_pre Pulse.Typing.wr Pulse.Typing.bind_comp_out Pulse.Syntax.Base.Tm_Bind Pulse.Syntax.Base.Mkst_term'__Tm_Bind__payload Pulse.Typing.T_Bind Pulse.Typing.bind_comp Pulse.Typing.Bind_comp FStar.Pervasives.dtuple3 Pulse.Syntax.Base.eq_tm Prims.bool Pulse.Typing.Env.fail FStar.Pervasives.Native.None Pulse.Syntax.Base.range Pulse.Syntax.Base.tm_emp_inames Pulse.Typing.T_Lift Pulse.Typing.Lift_STAtomic_ST Pulse.Syntax.Base.C_ST Pulse.Typing.bind_comp_ghost_l_out Pulse.Typing.Bind_comp_ghost_l Pulse.Typing.non_informative_t Pulse.Checker.Pure.get_non_informative_witness Pulse.Typing.bind_comp_ghost_r_out Pulse.Typing.Bind_comp_ghost_r FStar.Reflection.Typing.fstar_top_env Pulse.Typing.Env.fstar_env Pulse.Typing.Combinators.mk_bind Pulse.Typing.Lift_STGhost_STAtomic Pulse.Syntax.Base.C_STAtomic Pulse.Syntax.Base.binder Pulse.Typing.Combinators.nvar_as_binder FStar.Tactics.Types.proofstate Prims.l_and Pulse.Syntax.Base.comp_pre FStar.Pervasives.Native.uu___is_None Pulse.Syntax.Base.typ Pulse.Typing.Env.lookup Pulse.Syntax.Naming.freevars_st Pulse.Syntax.Naming.open_term Pulse.Syntax.Naming.freevars FStar.Tactics.Result.__result Prims.l_True
module Pulse.Typing.Combinators

module RT = FStar.Reflection.Typing
module R = FStar.Reflection.V2
module L = FStar.List.Tot
module T = FStar.Tactics.V2
module P = Pulse.Syntax.Printer

open FStar.List.Tot
open Pulse.Syntax
open Pulse.Typing
open Pulse.Checker.Pure

let rec vprop_equiv_typing (#g:_) (#t0 #t1:term) (v:vprop_equiv g t0 t1)
  : GTot ((tot_typing g t0 tm_vprop -> tot_typing g t1 tm_vprop) &
          (tot_typing g t1 tm_vprop -> tot_typing g t0 tm_vprop))
        (decreases v)
  = match v with
    | VE_Refl _ _ -> (fun x -> x), (fun x -> x)

    | VE_Sym _ _ _ v' -> 
      let f, g = vprop_equiv_typing v' in
      g, f

    | VE_Trans g t0 t2 t1 v02 v21 ->
      let f02, f20 = vprop_equiv_typing v02 in
      let f21, f12 = vprop_equiv_typing v21 in
      (fun x -> f21 (f02 x)), 
      (fun x -> f20 (f12 x))

    | VE_Ctxt g s0 s1 s0' s1' v0 v1 ->
      let f0, f0' = vprop_equiv_typing v0 in
      let f1, f1' = vprop_equiv_typing v1 in      
      let ff (x:tot_typing g (tm_star s0 s1) tm_vprop)
        : tot_typing g (tm_star s0' s1') tm_vprop
        = let s0_typing = star_typing_inversion_l x in
          let s1_typing = star_typing_inversion_r x in
          let s0'_typing, s1'_typing = f0 s0_typing, f1 s1_typing in
          star_typing s0'_typing s1'_typing
      in
      let gg (x:tot_typing g (tm_star s0' s1') tm_vprop)
        : tot_typing g (tm_star s0 s1) tm_vprop
        = let s0'_typing = star_typing_inversion_l x in
          let s1'_typing = star_typing_inversion_r x in
          star_typing (f0' s0'_typing) (f1' s1'_typing)        
      in
      ff, gg

    | VE_Unit g t ->
      let fwd (x:tot_typing g (tm_star tm_emp t) tm_vprop)
        : tot_typing g t tm_vprop
        = let r = star_typing_inversion_r x in
          r
      in
      let bk (x:tot_typing g t tm_vprop)
        : tot_typing g (tm_star tm_emp t) tm_vprop
        = star_typing emp_typing x
      in
      fwd, bk

    | VE_Comm g t0 t1 ->
      let f t0 t1 (x:tot_typing g (tm_star t0 t1) tm_vprop)
        : tot_typing g (tm_star t1 t0) tm_vprop
        = let tt0 = star_typing_inversion_l x in
          let tt1 = star_typing_inversion_r x in
          star_typing tt1 tt0
      in
      f t0 t1, f t1 t0

    | VE_Assoc g t0 t1 t2 ->
      let fwd (x:tot_typing g (tm_star t0 (tm_star t1 t2)) tm_vprop)
        : tot_typing g (tm_star (tm_star t0 t1) t2) tm_vprop
        = let tt0 = star_typing_inversion_l x in
          let tt12 = star_typing_inversion_r x in
          let tt1 = star_typing_inversion_l tt12 in
          let tt2 = star_typing_inversion_r tt12 in
          star_typing (star_typing tt0 tt1) tt2
      in
      let bk (x : tot_typing g (tm_star (tm_star t0 t1) t2) tm_vprop)
        : tot_typing g (tm_star t0 (tm_star t1 t2)) tm_vprop
        = let tt01 = star_typing_inversion_l x in
          let tt2 = star_typing_inversion_r x in
          let tt0 = star_typing_inversion_l tt01 in
          let tt1 = star_typing_inversion_r tt01 in
          star_typing tt0 (star_typing tt1 tt2)
      in
      fwd, bk
   
    | VE_Ext g t0 t1 token ->
      let d1, d2 = vprop_eq_typing_inversion g t0 t1 token in
      (fun _ -> d2),
      (fun _ -> d1)


#push-options "--z3rlimit_factor 8 --ifuel 1 --fuel 2 --query_stats"
let rec mk_bind (g:env)
                (pre:term)
                (e1:st_term)
                (e2:st_term)
                (c1:comp_st)
                (c2:comp_st)
                (px:nvar { ~ (Set.mem (snd px) (dom g)) })
                (d_e1:st_typing g e1 c1)
                (d_c1res:tot_typing g (comp_res c1) (tm_type (comp_u c1)))
                (d_e2:st_typing (push_binding g (snd px) (fst px) (comp_res c1)) (open_st_term_nv e2 px) c2)
                (res_typing:universe_of g (comp_res c2) (comp_u c2))
                (post_typing:tot_typing (push_binding g (snd px) (fst px) (comp_res c2))
                                        (open_term_nv (comp_post c2) px)
                                        tm_vprop)
  : T.TacH (t:st_term &
            c:comp_st { st_comp_of_comp c == st_comp_with_pre (st_comp_of_comp c2) pre } &
            st_typing g t c)
           (requires fun _ ->
              let _, x = px in
              comp_pre c1 == pre /\
              None? (lookup g x) /\
              (~(x `Set.mem` freevars_st e2)) /\
              open_term (comp_post c1) x == comp_pre c2 /\
val mk_bind (g:env)
            (pre:term)
            (e1:st_term)
            (e2:st_term)
            (c1:comp_st)
            (c2:comp_st)
            (px:nvar { ~ (Set.mem (snd px) (dom g)) })
            (d_e1:st_typing g e1 c1)
            (d_c1res:tot_typing g (comp_res c1) (tm_type (comp_u c1)))
            (d_e2:st_typing (push_binding g (snd px) (fst px) (comp_res c1)) (open_st_term_nv e2 px) c2)
            (res_typing:universe_of g (comp_res c2) (comp_u c2))
            (post_typing:tot_typing (push_binding g (snd px) (fst px) (comp_res c2))
                                     (open_term_nv (comp_post c2) px)
                                     tm_vprop)
  : T.TacH (t:st_term &
            c:comp_st { st_comp_of_comp c == st_comp_with_pre (st_comp_of_comp c2) pre } &
            st_typing g t c)
           (requires fun _ ->
              let _, x = px in
              comp_pre c1 == pre /\
              None? (lookup g x) /\
              (~(x `Set.mem` freevars_st e2)) /\
              open_term (comp_post c1) x == comp_pre c2 /\
              (~ (x `Set.mem` freevars (comp_post c2))))
           (ensures fun _ _ -> True)

    g: Pulse.Typing.Env.env ->
    pre: Pulse.Syntax.Base.term ->
    e1: Pulse.Syntax.Base.st_term ->
    e2: Pulse.Syntax.Base.st_term ->
    c1: Pulse.Syntax.Base.comp_st ->
    c2: Pulse.Syntax.Base.comp_st ->
    px:
      Pulse.Syntax.Base.nvar
        {~(FStar.Set.mem (FStar.Pervasives.Native.snd px) (Pulse.Typing.Env.dom g))} ->
    d_e1: Pulse.Typing.st_typing g e1 c1 ->
    d_c1res:
      Pulse.Typing.tot_typing g
        (Pulse.Syntax.Base.comp_res c1)
        (Pulse.Syntax.Pure.tm_type (Pulse.Syntax.Base.comp_u c1)) ->
    d_e2:
      Pulse.Typing.st_typing (Pulse.Typing.Env.push_binding g
            (FStar.Pervasives.Native.snd px)
            (FStar.Pervasives.Native.fst px)
            (Pulse.Syntax.Base.comp_res c1))
        (Pulse.Syntax.Naming.open_st_term_nv e2 px)
        c2 ->
    res_typing:
      Pulse.Typing.universe_of g (Pulse.Syntax.Base.comp_res c2) (Pulse.Syntax.Base.comp_u c2) ->
    post_typing:
      Pulse.Typing.tot_typing (Pulse.Typing.Env.push_binding g
            (FStar.Pervasives.Native.snd px)
            (FStar.Pervasives.Native.fst px)
            (Pulse.Syntax.Base.comp_res c2))
        (Pulse.Syntax.Naming.open_term_nv (Pulse.Syntax.Base.comp_post c2) px)
        Pulse.Syntax.Base.tm_vprop
  -> FStar.Tactics.Effect.TacH
    (FStar.Pervasives.dtuple3 Pulse.Syntax.Base.st_term
        (fun _ ->
            c:
            Pulse.Syntax.Base.comp_st
              { Pulse.Syntax.Base.st_comp_of_comp c ==
                Pulse.Typing.Combinators.st_comp_with_pre (Pulse.Syntax.Base.st_comp_of_comp c2) pre
              })
        (fun t c -> Pulse.Typing.st_typing g t c))