Definition subst_decl s k (d : context_decl) := map_decl (subst s k) d.

Inductive subs {cf:checker_flags} (Σ : global_env_ext) (Γ : context) : list term → context → Type :=
| emptys : subs Σ Γ [] []
| cons_ass Δ s na t T : subs Σ Γ s Δ → Σ ;;; Γ |- t : subst0 s T → subs Σ Γ (t :: s) (Δ ,, vass na T).

Inductive context_subst : context → list term → list term → Set :=
| context_subst_nil : context_subst [] [] []
| context_subst_ass Γ args s na t a :
    context_subst Γ args s →
    context_subst (vass na t :: Γ) (args ++ [a]) (a :: s)
| context_subst_def Γ args s na b t :
    context_subst Γ args s →
    context_subst (vdef na b t :: Γ) args (subst s 0 b :: s).

Fixpoint make_context_subst ctx args s :=
  match ctx with
  | [] ⇒ match args with
          | [] ⇒ Some s
          | a :: args ⇒ None
          end
  | d :: ctx ⇒
    match d.(decl_body) with
    | Some body ⇒ make_context_subst ctx args (subst0 s body :: s)
    | None ⇒ match args with
              | a :: args ⇒ make_context_subst ctx args (a :: s)
              | [] ⇒ None
              end
    end
  end.

Inductive subslet {cf:checker_flags} Σ (Γ : context) : list term → context → Type :=
| emptyslet : subslet Σ Γ [] []
| cons_let_ass Δ s na t T : subslet Σ Γ s Δ →
              Σ ;;; Γ |- t : subst0 s T →
             subslet Σ Γ (t :: s) (Δ ,, vass na T)
| cons_let_def Δ s na t T :
    subslet Σ Γ s Δ →
    Σ ;;; Γ |- subst0 s t : subst0 s T →
    subslet Σ Γ (subst0 s t :: s) (Δ ,, vdef na t T).

Lemma subslet_nth_error {cf:checker_flags} Σ Γ s Δ decl n t :
  subslet Σ Γ s Δ →
  nth_error Δ n = Some decl →
  nth_error s n = Some t →
  match decl_body decl return Type with
  | Some t' ⇒
    let b := subst0 (skipn (S n) s) t' in
    let ty := subst0 (skipn (S n) s) (decl_type decl) in
    ((t = b) × (Σ ;;; Γ |- b : ty))%type
  | None ⇒
    let ty := subst0 (skipn (S n) s) (decl_type decl) in
    Σ ;;; Γ |- t : ty
  end.

Lemma subslet_length {cf:checker_flags} {Σ Γ s Δ} : subslet Σ Γ s Δ → #|s| = #|Δ|.

Lemma subst_decl0 k d : map_decl (subst [] k) d = d.

Lemma subst0_context k Γ : subst_context [] k Γ = Γ.

Lemma fold_context_length f Γ : #|fold_context f Γ| = #|Γ|.

Lemma subst_context_length s k Γ : #|subst_context s k Γ| = #|Γ|.

Lemma subst_context_snoc s k Γ d : subst_context s k (d :: Γ) = subst_context s k Γ ,, subst_decl s (#|Γ| + k) d.

Lemma subst_context_snoc0 s Γ d : subst_context s 0 (Γ ,, d) = subst_context s 0 Γ ,, subst_decl s #|Γ| d.

Lemma subst_context_alt s k Γ :
  subst_context s k Γ =
  mapi (fun k' d ⇒ subst_decl s (Nat.pred #|Γ| - k' + k) d) Γ.

Lemma subst_context_app s k Γ Δ :
  subst_context s k (Γ ,,, Δ) = subst_context s k Γ ,,, subst_context s (#|Γ| + k) Δ.

Lemma map_vass_map_def_subst g l n k :
  (mapi (fun i (d : def term) ⇒ vass (dname d) (lift0 i (dtype d)))
        (map (map_def (subst n k) g) l)) =
  (mapi (fun i d ⇒ map_decl (subst n (i + k)) d) (mapi (fun i (d : def term) ⇒ vass (dname d) (lift0 i (dtype d))) l)).

Lemma All_local_env_subst {cf:checker_flags} (P Q : context → term → option term → Type) c n k :
  All_local_env Q c →
  (∀ Γ t T,
      Q Γ t T →
      P (subst_context n k Γ) (subst n (#|Γ| + k) t)
        (option_map (subst n (#|Γ| + k)) T)
  ) →
  All_local_env P (subst_context n k c).

Lemma subst_length {cf:checker_flags} Σ Γ s Γ' : subs Σ Γ s Γ' → #|s| = #|Γ'|.

Lemma subs_nth_error_ge {cf:checker_flags} Σ Γ Γ' Γ'' v s :
  subs Σ Γ s Γ' →
  #|Γ' ,,, Γ''| ≤ v →
  nth_error (Γ ,,, Γ' ,,, Γ'') v =
  nth_error (Γ ,,, subst_context s 0 Γ'') (v - #|Γ'|).

Lemma nth_error_subst_context (Γ' : context) s (v : nat) k :
    nth_error (subst_context s k Γ') v =
    option_map (subst_decl s (#|Γ'| - S v + k)) (nth_error Γ' v).

Lemma subs_nth_error_lt {cf:checker_flags} Σ Γ Γ' Γ'' v s :
  subs Σ Γ s Γ' →
  v < #|Γ''| →
  nth_error (Γ ,,, subst_context s 0 Γ'') v =
  option_map (map_decl (subst s (#|Γ''| - S v))) (nth_error (Γ ,,, Γ' ,,, Γ'') v).

Lemma subslet_nth_error_lt {cf:checker_flags} Σ Γ Γ' Γ'' v s :
  subslet Σ Γ s Γ' →
  v < #|Γ''| →
  nth_error (Γ ,,, subst_context s 0 Γ'') v =
  option_map (map_decl (subst s (#|Γ''| - S v))) (nth_error (Γ ,,, Γ' ,,, Γ'') v).

Lemma subst_iota_red s k pars c args brs :
  subst s k (iota_red pars c args brs) =
  iota_red pars c (List.map (subst s k) args) (List.map (on_snd (subst s k)) brs).

Lemma subst_unfold_fix n k mfix idx narg fn :
  unfold_fix mfix idx = Some (narg, fn) →
  unfold_fix (map (map_def (subst n k) (subst n (#|mfix| + k))) mfix) idx = Some (narg, subst n k fn).

Lemma subst_unfold_cofix n k mfix idx narg fn :
  unfold_cofix mfix idx = Some (narg, fn) →
  unfold_cofix (map (map_def (subst n k) (subst n (#|mfix| + k))) mfix) idx = Some (narg, subst n k fn).

Lemma decompose_app_rec_subst n k t l :
  let (f, a) := decompose_app_rec t l in
  subst n k f = f →
  decompose_app_rec (subst n k t) (map (subst n k) l) = (f, map (subst n k) a).

Lemma decompose_app_subst n k t f a :
  decompose_app t = (f, a) → subst n k f = f →
  decompose_app (subst n k t) = (subst n k f, map (subst n k) a).

Lemma subst_is_constructor:
  ∀ (args : list term) (narg : nat) n k,
    is_constructor narg args = true → is_constructor narg (map (subst n k) args) = true.

Lemma typed_subst `{checker_flags} Σ Γ t T n k :
  wf Σ.1 → k ≥ #|Γ| →
  Σ ;;; Γ |- t : T → subst n k T = T ∧ subst n k t = t.

Lemma subst_wf_local `{checker_flags} Σ Γ n k :
  wf Σ.1 →
  wf_local Σ Γ →
  subst_context n k Γ = Γ.

Lemma subst_declared_constant `{H:checker_flags} Σ cst decl n k u :
  wf Σ →
  declared_constant Σ cst decl →
  map_constant_body (subst n k) (map_constant_body (subst_instance_constr u) decl) =
  map_constant_body (subst_instance_constr u) decl.

Definition subst_mutual_inductive_body n k m :=
  map_mutual_inductive_body (fun k' ⇒ subst n (k' + k)) m.


Lemma subst_declared_minductive {cf:checker_flags} Σ cst decl n k :
  wf Σ →
  declared_minductive Σ cst decl →
  subst_mutual_inductive_body n k decl = decl.

Lemma subst_declared_inductive {cf:checker_flags} Σ ind mdecl idecl n k :
  wf Σ →
  declared_inductive Σ mdecl ind idecl →
  map_one_inductive_body (context_assumptions mdecl.(ind_params))
                         (length (arities_context mdecl.(ind_bodies)))
                         (fun k' ⇒ subst n (k' + k)) (inductive_ind ind) idecl = idecl.

Lemma subst0_inds_subst ind u mdecl n k t :
  (subst0 (inds (inductive_mind ind) u (ind_bodies mdecl))
          (subst n (#|arities_context (ind_bodies mdecl)| + k) t)) =
  subst n k (subst0 (inds (inductive_mind ind) u (ind_bodies mdecl)) t).

Lemma subst_declared_constructor {cf:checker_flags} Σ c u mdecl idecl cdecl n k :
  wf Σ → declared_constructor Σ mdecl idecl c cdecl →
  subst (map (subst_instance_constr u) n) k (type_of_constructor mdecl cdecl c u) = (type_of_constructor mdecl cdecl c u).

Lemma subst_declared_projection {cf:checker_flags} Σ c mdecl idecl pdecl n k :
  wf Σ →
  declared_projection Σ mdecl idecl c pdecl →
  on_snd (subst n (S (ind_npars mdecl + k))) pdecl = pdecl.

Lemma subst_fix_context:
  ∀ (mfix : list (def term)) n (k : nat),
    fix_context (map (map_def (subst n k) (subst n (#|mfix| + k))) mfix) =
    subst_context n k (fix_context mfix).

Lemma subst_destArity ctx t n k :
  match destArity ctx t with
  | Some (args, s) ⇒
    destArity (subst_context n k ctx) (subst n (#|ctx| + k) t) = Some (subst_context n k args, s)
  | None ⇒ True
  end.

Lemma decompose_prod_n_assum0 ctx t : decompose_prod_n_assum ctx 0 t = Some (ctx, t).

Lemma subst_instantiate_params_subst n k params args s t :
  ∀ s' t',
    instantiate_params_subst params args s t = Some (s', t') →
    instantiate_params_subst
      (mapi_rec (fun k' decl ⇒ subst_decl n (k' + k) decl) params #|s|)
      (map (subst n k) args) (map (subst n k) s) (subst n (#|s| + k) t) =
    Some (map (subst n k) s', subst n (#|s| + k + #|params|) t').

Lemma subst_decl_closed n k d : closed_decl k d → subst_decl n k d = d.

Lemma closed_ctx_subst n k ctx : closed_ctx ctx = true → subst_context n k ctx = ctx.

Lemma closed_tele_subst n k ctx :
  closed_ctx ctx →
  mapi (fun (k' : nat) (decl : context_decl) ⇒ subst_decl n (k' + k) decl) (List.rev ctx) = List.rev ctx.

Lemma decompose_prod_n_assum_extend_ctx {ctx n t ctx' t'} ctx'' :
  decompose_prod_n_assum ctx n t = Some (ctx', t') →
  decompose_prod_n_assum (ctx ++ ctx'') n t = Some (ctx' ++ ctx'', t').

Lemma subst_it_mkProd_or_LetIn n k ctx t :
  subst n k (it_mkProd_or_LetIn ctx t) =
  it_mkProd_or_LetIn (subst_context n k ctx) (subst n (length ctx + k) t).

Lemma to_extended_list_k_subst n k c k' :
  to_extended_list_k (subst_context n k c) k' = to_extended_list_k c k'.

Lemma to_extended_list_k_map_subst:
  ∀ n (k : nat) (c : context) k',
    #|c| + k' ≤ k →
    to_extended_list_k c k' = map (subst n k) (to_extended_list_k c k').

Lemma subst_instantiate_params n k params args t ty :
  closed_ctx params →
  instantiate_params params args t = Some ty →
  instantiate_params params (map (subst n k) args) (subst n k t) = Some (subst n k ty).

Lemma wf_arities_context' {cf:checker_flags}:
  ∀ (Σ : global_env_ext) (mind : ident) (mdecl : mutual_inductive_body),
    wf Σ →
    on_inductive (lift_typing typing) Σ mind mdecl →
    wf_local Σ (arities_context (ind_bodies mdecl)).

Lemma wf_arities_context {cf:checker_flags} Σ mind mdecl : wf Σ →
  declared_minductive Σ mind mdecl → wf_local (Σ, ind_universes mdecl) (arities_context mdecl.(ind_bodies)).

Lemma on_constructor_closed {cf:checker_flags} {Σ mind mdecl u i idecl cdecl} :
  wf Σ →
  on_constructor (lift_typing typing) (Σ, ind_universes mdecl) (inductive_mind mind) mdecl (inductive_ind mind) idecl i cdecl →
  let cty := subst0 (inds (inductive_mind mind) u (ind_bodies mdecl))
                    (subst_instance_constr u (snd (fst cdecl)))
  in closed cty.

Lemma on_projection_closed {cf:checker_flags} {Σ mind mdecl u i idecl pdecl} :
  wf Σ → mdecl.(ind_npars) = context_assumptions mdecl.(ind_params) →
  on_projection (lift_typing typing) (Σ, ind_universes mdecl) (inductive_mind mind) mdecl (inductive_ind mind) idecl i pdecl →
  let pty := subst_instance_constr u (snd pdecl) in
  closedn (S (ind_npars mdecl)) pty.

Lemma context_subst_length Γ a s : context_subst Γ a s → #|Γ| = #|s|.

Lemma context_subst_assumptions_length Γ a s : context_subst Γ a s → context_assumptions Γ = #|a|.



Lemma make_context_subst_rec_spec ctx args s tele args' s' :
  context_subst ctx args s →
  make_context_subst tele args' s = Some s' →
  context_subst (List.rev tele ++ ctx) (args ++ args') s'.

Lemma make_context_subst_spec tele args s' :
  make_context_subst tele args [] = Some s' →
  context_subst (List.rev tele) args s'.

Lemma instantiate_params_subst_make_context_subst ctx args s ty s' ty' :
  instantiate_params_subst ctx args s ty = Some (s', ty') →
  ∑ ctx'',
  make_context_subst ctx args s = Some s' ∧
  decompose_prod_n_assum [] (length ctx) ty = Some (ctx'', ty').

Lemma instantiate_params_make_context_subst ctx args ty ty' :
  instantiate_params ctx args ty = Some ty' →
  ∑ ctx' ty'' s',
    decompose_prod_n_assum [] (length ctx) ty = Some (ctx', ty'') ∧
    make_context_subst (List.rev ctx) args [] = Some s' ∧ ty' = subst0 s' ty''.

Lemma subst_cstr_concl_head ind u mdecl (arity : context) args :
  let head := tRel (#|ind_bodies mdecl| - S (inductive_ind ind) + #|ind_params mdecl| + #|arity|) in
  let s := (inds (inductive_mind ind) u (ind_bodies mdecl)) in
  inductive_ind ind < #|ind_bodies mdecl| →
  subst s (#|arity| + #|ind_params mdecl|)
        (subst_instance_constr u (mkApps head (to_extended_list_k (ind_params mdecl) #|arity| ++ args)))
  = mkApps (tInd ind u) (to_extended_list_k (ind_params mdecl) #|arity| ++
                        map (subst s (#|arity| + #|ind_params mdecl|)) (map (subst_instance_constr u) args)).

Lemma subst_to_extended_list_k s k args ctx :
  make_context_subst (List.rev ctx) args [] = Some s →
  map (subst s k) (to_extended_list_k ctx k) = map (lift0 k) args.

Lemma Alli_map_option_out_mapi_Some_spec' {A B} (f g : nat → A → option B) h l t P :
  Alli P 0 l →
  (∀ i x t, P i x → f i x = Some t → g i x = Some (h t)) →
  map_option_out (mapi f l) = Some t →
  map_option_out (mapi g l) = Some (map h t).

Lemma map_subst_instance_constr_to_extended_list_k u ctx k :
  to_extended_list_k (subst_instance_context u ctx) k
  = to_extended_list_k ctx k.

Lemma subst_instance_context_assumptions u ctx :
  context_assumptions (subst_instance_context u ctx)
  = context_assumptions ctx.

Lemma subst_build_branches_type {cf:checker_flags}
      n k Σ ind mdecl idecl args u p brs :
  wf Σ →
  declared_inductive Σ mdecl ind idecl →
  closed_ctx (subst_instance_context u (ind_params mdecl)) →
  on_inductive (lift_typing typing) (Σ, ind_universes mdecl)
               (inductive_mind ind) mdecl →
  on_constructors (lift_typing typing) (Σ, ind_universes mdecl)
            (inductive_mind ind) mdecl (inductive_ind ind) idecl
            (ind_ctors idecl) →
  map_option_out (build_branches_type ind mdecl idecl args u p) = Some brs →
  map_option_out (build_branches_type ind mdecl
         idecl (map (subst n k) args) u (subst n k p)) =
         Some (map (on_snd (subst n k)) brs).

Lemma subst_types_of_case {cf:checker_flags} (Σ : global_env) ind mdecl idecl args u p pty indctx pctx ps btys n k :
  let f (ctx : context) := subst n (#|ctx| + k) in
  let f_ctx := subst_context n k in
  wf Σ →
  declared_inductive Σ mdecl ind idecl →
  types_of_case ind mdecl idecl args u p pty = Some (indctx, pctx, ps, btys) →
  types_of_case ind mdecl idecl (map (f []) args) u (f [] p) (f [] pty) =
  Some (f_ctx indctx, f_ctx pctx, ps, map (on_snd (f [])) btys).


Inductive untyped_subslet (Γ : context) : list term → context → Type :=
| untyped_emptyslet : untyped_subslet Γ [] []
| untyped_cons_let_ass Δ s na t T :
    untyped_subslet Γ s Δ →
    untyped_subslet Γ (t :: s) (Δ ,, vass na T)
| untyped_cons_let_def Δ s na t T :
    untyped_subslet Γ s Δ →
    untyped_subslet Γ (subst0 s t :: s) (Δ ,, vdef na t T).

Lemma subs_nth_error {cf:checker_flags} Σ Γ s Δ decl n t :
  subs Σ Γ s Δ →
  nth_error Δ n = Some decl →
  nth_error s n = Some t →
  match decl_body decl return Type with
  | Some t' ⇒ False
  | None ⇒
    let ty := subst0 (skipn (S n) s) (decl_type decl) in
    Σ ;;; Γ |- t : ty
  end.

Lemma untyped_subslet_nth_error Γ s Δ decl n t :
  untyped_subslet Γ s Δ →
  nth_error Δ n = Some decl →
  nth_error s n = Some t →
  match decl_body decl return Type with
  | Some t' ⇒ t = subst0 (skipn (S n) s) t'
  | None ⇒ True
  end.






Lemma red1_mkApps_l Σ Γ M1 N1 M2 :
  red1 Σ Γ M1 N1 → red1 Σ Γ (mkApps M1 M2) (mkApps N1 M2).

Lemma red1_mkApps_r Σ Γ M1 M2 N2 :
  OnOne2 (red1 Σ Γ) M2 N2 → red1 Σ Γ (mkApps M1 M2) (mkApps M1 N2).


Lemma substitution_red1 {cf:checker_flags} (Σ : global_env_ext) Γ Γ' Γ'' s M N :
  wf Σ → subs Σ Γ s Γ' → wf_local Σ Γ →
  red1 Σ (Γ ,,, Γ' ,,, Γ'') M N →
  red1 Σ (Γ ,,, subst_context s 0 Γ'') (subst s #|Γ''| M) (subst s #|Γ''| N).

Lemma subst_skipn n s k t : n ≤ #|s| → subst (skipn n s) k t = subst s k (lift n k t).


Lemma substitution_let_red `{cf : checker_flags} (Σ : global_env_ext) Γ Δ Γ' s M N :
  wf Σ → subslet Σ Γ s Δ → wf_local Σ Γ →
  red1 Σ (Γ ,,, Δ ,,, Γ') M N →
  red Σ (Γ ,,, subst_context s 0 Γ') (subst s #|Γ'| M) (subst s #|Γ'| N).

Lemma untyped_substlet_length {Γ s Δ} : untyped_subslet Γ s Δ → #|s| = #|Δ|.

Lemma substitution_untyped_let_red {cf:checker_flags} Σ Γ Δ Γ' s M N :
  wf Σ → untyped_subslet Γ s Δ →
  red1 Σ (Γ ,,, Δ ,,, Γ') M N →
  red Σ (Γ ,,, subst_context s 0 Γ') (subst s #|Γ'| M) (subst s #|Γ'| N).

Lemma subst_eq_decl `{checker_flags} ϕ l k d d' :
  eq_decl ϕ d d' → eq_decl ϕ (subst_decl l k d) (subst_decl l k d').

Lemma subst_eq_context `{checker_flags} φ l l' n k :
  eq_context φ l l' →
  eq_context φ (subst_context n k l) (subst_context n k l').

Lemma subst_check_correct_arity:
  ∀ (cf : checker_flags) φ (ind : inductive) (u : universe_instance)
         (npar : nat) (args : list term) (idecl : one_inductive_body)
         (indctx pctx : list context_decl) s k,
    check_correct_arity φ idecl ind u indctx (firstn npar args) pctx →
    check_correct_arity
      φ idecl ind u (subst_context s k indctx) (firstn npar (map (subst s k) args))
      (subst_context s k pctx).

Lemma substitution_red `{cf : checker_flags} (Σ : global_env_ext) Γ Δ Γ' s M N :
  wf Σ → subslet Σ Γ s Δ → wf_local Σ Γ →
  red Σ (Γ ,,, Δ ,,, Γ') M N →
  red Σ (Γ ,,, subst_context s 0 Γ') (subst s #|Γ'| M) (subst s #|Γ'| N).

Lemma red_red {cf:checker_flags} (Σ : global_env_ext) Γ Δ Γ' s s' b : wf Σ →
  All2 (red Σ Γ) s s' →
  untyped_subslet Γ s Δ →
  red Σ (Γ ,,, Γ') (subst s #|Γ'| b) (subst s' #|Γ'| b).

Lemma untyped_substitution_red {cf:checker_flags} Σ Γ Δ Γ' s M N :
  wf Σ → untyped_subslet Γ s Δ →
  red Σ (Γ ,,, Δ ,,, Γ') M N →
  red Σ (Γ ,,, subst_context s 0 Γ') (subst s #|Γ'| M) (subst s #|Γ'| N).

Lemma substitution_untyped_cumul {cf:checker_flags} Σ Γ Γ' Γ'' s M N :
  wf Σ.1 → untyped_subslet Γ s Γ' →
  Σ ;;; Γ ,,, Γ' ,,, Γ'' |- M ≤ N →
  Σ ;;; Γ ,,, subst_context s 0 Γ'' |- subst s #|Γ''| M ≤ subst s #|Γ''| N.

Lemma substitution_cumul0 {cf:checker_flags} Σ Γ na t u u' a : wf Σ.1 →
  Σ ;;; Γ ,, vass na t |- u ≤ u' →
  Σ ;;; Γ |- subst10 a u ≤ subst10 a u'.

Lemma substitution_cumul `{cf : checker_flags} (Σ : global_env_ext) Γ Γ' Γ'' s M N :
  wf Σ → wf_local Σ (Γ ,,, Γ' ,,, Γ'') → subslet Σ Γ s Γ' →
  Σ ;;; Γ ,,, Γ' ,,, Γ'' |- M ≤ N →
  Σ ;;; Γ ,,, subst_context s 0 Γ'' |- subst s #|Γ''| M ≤ subst s #|Γ''| N.

Theorem substitution `{cf : checker_flags} (Σ : global_env_ext) Γ Γ' s Δ (t : term) T :
  wf Σ → subslet Σ Γ s Γ' →
  Σ ;;; Γ ,,, Γ' ,,, Δ |- t : T →
  wf_local Σ (Γ ,,, subst_context s 0 Δ) →
  Σ ;;; Γ ,,, subst_context s 0 Δ |- subst s #|Δ| t : subst s #|Δ| T.

Theorem substitution_alt {cf:checker_flags} (Σ : global_env_ext) Γ Γ' s Δ (t : term) T :
  wf Σ →
  subslet Σ Γ s Γ' →
  Σ ;;; Γ ,,, Γ' ,,, Δ |- t : T →
  Σ ;;; Γ ,,, subst_context s 0 Δ |- subst s #|Δ| t : subst s #|Δ| T.

Lemma substitution0 {cf:checker_flags} (Σ : global_env_ext) Γ n u U (t : term) T :
  wf Σ →
  Σ ;;; Γ ,, vass n U |- t : T → Σ ;;; Γ |- u : U →
  Σ ;;; Γ |- t {0 := u} : T {0 := u}.

Lemma substitution_let {cf:checker_flags} (Σ : global_env_ext) Γ n u U (t : term) T :
  wf Σ →
  Σ ;;; Γ ,, vdef n u U |- t : T →
  Σ ;;; Γ |- t {0 := u} : T {0 := u}.