val st_typing_weakening_end
  (g:env) (g':env { disjoint g g' })
  (t:st_term) (c:comp) (d:st_typing (push_env g g') t c)
  (g'':env { g'' `env_extends` g' /\ disjoint g'' g })
  : st_typing (push_env g g'') t c
let st_typing_weakening_end
  (g:env) (g':env { disjoint g g' })
  (t:st_term) (c:comp) (d:st_typing (push_env g g') t c)
  (g'':env { g'' `env_extends` g' /\ disjoint g'' g })
  : st_typing (push_env g g'') t c =

  let g2 = diff g'' g' in
  let emp_env = mk_env (fstar_env g) in
  assert (equal (push_env g g')
                (push_env (push_env g g') emp_env));
  let d
    : st_typing (push_env (push_env (push_env g g') g2) emp_env) _ _
    = Pulse.Typing.Metatheory.Base.st_typing_weakening (push_env g g') emp_env t c (coerce_eq () d) g2 in
  assert (equal (push_env (push_env (push_env g g') g2) emp_env)
                (push_env (push_env g g') g2));
  push_env_assoc g g' g2;
  assert (equal (push_env (push_env g g') g2)
                (push_env g (push_env g' g2)));
  assert (equal (push_env g (push_env g' g2))
                (push_env g g''));
  coerce_eq () d
val st_typing_weakening_end
  (g:env) (g':env { disjoint g g' })
  (t:st_term) (c:comp) (d:st_typing (push_env g g') t c)
  (g'':env { g'' `env_extends` g' /\ disjoint g'' g })
  : st_typing (push_env g g'') t c
let st_typing_weakening_end
      (g: env)
      (g': env{disjoint g g'})
      (t: st_term)
      (c: comp)
      (d: st_typing (push_env g g') t c)
      (g'': env{g'' `env_extends` g' /\ disjoint g'' g})
    : st_typing (push_env g g'') t c =
let g2 = diff g'' g' in
let emp_env = mk_env (fstar_env g) in
assert (equal (push_env g g') (push_env (push_env g g') emp_env));
let d:st_typing (push_env (push_env (push_env g g') g2) emp_env) _ _ =
  Pulse.Typing.Metatheory.Base.st_typing_weakening (push_env g g') emp_env t c (coerce_eq () d) g2
in
assert (equal (push_env (push_env (push_env g g') g2) emp_env) (push_env (push_env g g') g2));
push_env_assoc g g' g2;
assert (equal (push_env (push_env g g') g2) (push_env g (push_env g' g2)));
assert (equal (push_env g (push_env g' g2)) (push_env g g''));
coerce_eq () d
Pulse.Typing.Metatheory.fst.checked
Pulse.Typing.Metatheory.Base.fsti.checked Pulse.Typing.fst.checked Pulse.Syntax.fst.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Pervasives.fsti.checked
Pulse.Typing.Metatheory.fst
Pulse.Typing.Env.env Pulse.Typing.Env.disjoint Pulse.Syntax.Base.st_term Pulse.Syntax.Base.comp Pulse.Typing.st_typing Pulse.Typing.Env.push_env Prims.l_and Pulse.Typing.Env.env_extends FStar.Pervasives.coerce_eq Prims.unit Prims._assert Pulse.Typing.Env.equal Pulse.Typing.Env.push_env_assoc Pulse.Typing.Metatheory.Base.st_typing_weakening Prims.eq2 FStar.Reflection.Typing.fstar_top_env Pulse.Typing.Env.fstar_env Pulse.Typing.Env.mk_env Pulse.Typing.Env.diff
module Pulse.Typing.Metatheory

open Pulse.Syntax
open Pulse.Typing

module T = FStar.Tactics.V2

let tot_typing_weakening_single #g #t #ty d x x_t =
  let g1 = singleton_env (fstar_env g) x x_t in
  let g' = mk_env (fstar_env g) in
  assert (equal (push_env g g') g);
  assert (equal (push_env (push_env g g1) g') (push_env g g1));
  assert (equal (push_env g g1) (push_binding g x ppname_default x_t));
  tot_typing_weakening g g' t ty d g1

let tot_typing_weakening_standard g #t #ty d g2 =
  let g1 = diff g2 g in
  let g' = mk_env (fstar_env g) in
  assert (equal (push_env g g1) g2);
  assert (equal (push_env g g') g);
  assert (equal (push_env (push_env g g1) g') g2);
  tot_typing_weakening g g' t ty d g1

let st_typing_weakening
  (g:env) (g':env { disjoint g g' })
  (t:st_term) (c:comp) (d:st_typing (push_env g g') t c)
  (g1:env { g1 `env_extends` g /\ disjoint g1 g' })
  : st_typing (push_env g1 g') t c =

  let g2 = diff g1 g in
  let d = st_typing_weakening g g' t c d g2 in
  assert (equal (push_env (push_env g g2) g') (push_env g1 g'));
  d

let st_typing_weakening_standard
  (#g:env) (#t:st_term) (#c:comp) (d:st_typing g t c)
  (g1:env { g1 `env_extends` g })
  : st_typing g1 t c =

  let g' = mk_env (fstar_env g) in
  assert (equal (push_env g g') g);
  let d = st_typing_weakening g g' t c d g1 in
  assert (equal (push_env g1 g') g1);
  d

let st_typing_weakening_end
  (g:env) (g':env { disjoint g g' })
  (t:st_term) (c:comp) (d:st_typing (push_env g g') t c)
val st_typing_weakening_end
  (g:env) (g':env { disjoint g g' })
  (t:st_term) (c:comp) (d:st_typing (push_env g g') t c)
  (g'':env { g'' `env_extends` g' /\ disjoint g'' g })
  : st_typing (push_env g g'') t c

    g: Pulse.Typing.Env.env ->
    g': Pulse.Typing.Env.env{Pulse.Typing.Env.disjoint g g'} ->
    t: Pulse.Syntax.Base.st_term ->
    c: Pulse.Syntax.Base.comp ->
    d: Pulse.Typing.st_typing (Pulse.Typing.Env.push_env g g') t c ->
    g'':
      Pulse.Typing.Env.env{Pulse.Typing.Env.env_extends g'' g' /\ Pulse.Typing.Env.disjoint g'' g}
  -> Pulse.Typing.st_typing (Pulse.Typing.Env.push_env g g'') t c