val tot_typing_weakening_single (#g:env) (#t #ty:term)
  (d:tot_typing g t ty)
  (x:var { ~ (x `Set.mem` dom g)})
  (x_t:typ)

  : tot_typing (push_binding g x ppname_default x_t) t ty
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_single (#g:env) (#t #ty:term)
  (d:tot_typing g t ty)
  (x:var { ~ (x `Set.mem` dom g)})
  (x_t:typ)

  : tot_typing (push_binding g x ppname_default x_t) t ty
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
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.Syntax.Base.var Prims.l_not Prims.b2t FStar.Set.mem Pulse.Typing.Env.dom Pulse.Syntax.Base.typ Pulse.Typing.Metatheory.Base.tot_typing_weakening Prims.unit Prims._assert Pulse.Typing.Env.equal Pulse.Typing.Env.push_env Pulse.Typing.Env.push_binding Pulse.Syntax.Base.ppname_default Prims.eq2 FStar.Reflection.Typing.fstar_top_env Pulse.Typing.Env.fstar_env Pulse.Typing.Env.mk_env Pulse.Typing.Env.singleton_env
module Pulse.Typing.Metatheory

open Pulse.Syntax
open Pulse.Typing

module T = FStar.Tactics.V2
val tot_typing_weakening_single (#g:env) (#t #ty:term)
  (d:tot_typing g t ty)
  (x:var { ~ (x `Set.mem` dom g)})
  (x_t:typ)

  : tot_typing (push_binding g x ppname_default x_t) t ty

    d: Pulse.Typing.tot_typing g t ty ->
    x: Pulse.Syntax.Base.var{~(FStar.Set.mem x (Pulse.Typing.Env.dom g))} ->
    x_t: Pulse.Syntax.Base.typ
  -> Pulse.Typing.tot_typing (Pulse.Typing.Env.push_binding g x Pulse.Syntax.Base.ppname_default x_t
      )
      t
      ty