val tot_typing_weakening_standard (g:env)
  (#t #ty:term) (d:tot_typing g t ty)
  (g1:env { g1 `env_extends` g })
  : tot_typing g1 t ty
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
val tot_typing_weakening_standard (g:env)
  (#t #ty:term) (d:tot_typing g t ty)
  (g1:env { g1 `env_extends` g })
  : tot_typing g1 t ty
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
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.Syntax.Base.term Pulse.Typing.tot_typing Pulse.Typing.Env.env_extends Pulse.Typing.Metatheory.Base.tot_typing_weakening Prims.unit Prims._assert Pulse.Typing.Env.equal Pulse.Typing.Env.push_env 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
val tot_typing_weakening_standard (g:env)
  (#t #ty:term) (d:tot_typing g t ty)
  (g1:env { g1 `env_extends` g })
  : tot_typing g1 t ty

    g: Pulse.Typing.Env.env ->
    d: Pulse.Typing.tot_typing g t ty ->
    g1: Pulse.Typing.Env.env{Pulse.Typing.Env.env_extends g1 g}
  -> Pulse.Typing.tot_typing g1 t ty