Lemma global_ext_constraints_app Σ Σ' φ
  : ConstraintSet.Subset (global_ext_constraints (Σ, φ))
                         (global_ext_constraints (Σ' ++ Σ, φ)).

Lemma leq_universe_subset {cf:checker_flags} ctrs ctrs' t u
  : ConstraintSet.Subset ctrs ctrs' → leq_universe ctrs t u → leq_universe ctrs' t u.

Lemma eq_universe_subset {cf:checker_flags} ctrs ctrs' t u
  : ConstraintSet.Subset ctrs ctrs'
    → eq_universe ctrs t u → eq_universe ctrs' t u.

Lemma leq_term_subset {cf:checker_flags} ctrs ctrs' t u
  : ConstraintSet.Subset ctrs ctrs' → leq_term ctrs t u → leq_term ctrs' t u.

Definition extends (Σ Σ' : global_env) :=
  { Σ'' & Σ' = (Σ'' ++ Σ)%list }.

Lemma weakening_env_global_ext_levels Σ Σ' φ (H : extends Σ Σ') l
  : LevelSet.In l (global_ext_levels (Σ, φ))
    → LevelSet.In l (global_ext_levels (Σ', φ)).

Lemma weakening_env_global_ext_levels' Σ Σ' φ (H : extends Σ Σ') l
  : LevelSet.mem l (global_ext_levels (Σ, φ))
    → LevelSet.mem l (global_ext_levels (Σ', φ)).

Lemma weakening_env_global_ext_constraints Σ Σ' φ (H : extends Σ Σ')
  : ConstraintSet.Subset (global_ext_constraints (Σ, φ))
                         (global_ext_constraints (Σ', φ)).

Lemma eq_term_subset {cf:checker_flags} φ φ' t t'
  : ConstraintSet.Subset φ φ'
    → eq_term φ t t' → eq_term φ' t t'.

Lemma eq_decl_subset {cf:checker_flags} φ φ' d d'
  : ConstraintSet.Subset φ φ'
    → eq_decl φ d d' → eq_decl φ' d d'.

Lemma eq_context_subset {cf:checker_flags} φ φ' Γ Γ'
  : ConstraintSet.Subset φ φ'
    → eq_context φ Γ Γ' → eq_context φ' Γ Γ'.

Lemma check_correct_arity_subset {cf:checker_flags} φ φ' decl ind u ctx pars pctx
  : ConstraintSet.Subset φ φ' → check_correct_arity φ decl ind u ctx pars pctx
    → check_correct_arity φ' decl ind u ctx pars pctx.



Lemma lookup_env_Some_fresh `{checker_flags} Σ c decl :
  lookup_env Σ c = Some decl → ¬ (fresh_global c Σ).

Lemma extends_lookup `{checker_flags} Σ Σ' c decl :
  wf Σ' → extends Σ Σ' → lookup_env Σ c = Some decl → lookup_env Σ' c = Some decl.

Lemma extends_wf_local `{checker_flags} Σ Γ (wfΓ : wf_local Σ Γ) :
  All_local_env_over typing
      (fun Σ0 Γ0 wfΓ (t T : term) ty ⇒
         ∀ Σ' : global_env,
           wf Σ' →
           extends Σ0 Σ' →
           (Σ', Σ0.2);;; Γ0 |- t : T
      ) Σ Γ wfΓ →
    ∀ Σ' : global_env, wf Σ' → extends Σ Σ' → wf_local (Σ', Σ.2) Γ.

Lemma weakening_env_red1 `{CF:checker_flags} Σ Σ' Γ M N :
  wf Σ' → extends Σ Σ' →
  red1 Σ Γ M N →
  red1 Σ' Γ M N.

Lemma weakening_env_cumul `{CF:checker_flags} Σ Σ' φ Γ M N :
  wf Σ' → extends Σ Σ' →
  cumul (Σ, φ) Γ M N → cumul (Σ', φ) Γ M N.

Lemma weakening_env_declared_constant `{CF:checker_flags}:
  ∀ (Σ : global_env) (cst : ident) (decl : constant_body),
    declared_constant Σ cst decl →
    ∀ Σ' : global_env, wf Σ' → extends Σ Σ' → declared_constant Σ' cst decl.

Lemma weakening_env_declared_minductive `{CF:checker_flags}:
  ∀ (Σ : global_env) ind decl,
    declared_minductive Σ ind decl →
    ∀ Σ' : global_env, wf Σ' → extends Σ Σ' → declared_minductive Σ' ind decl.

Lemma weakening_env_declared_inductive:
  ∀ (H : checker_flags) (Σ : global_env) ind mdecl decl,
    declared_inductive Σ ind mdecl decl →
    ∀ Σ' : global_env, wf Σ' → extends Σ Σ' → declared_inductive Σ' ind mdecl decl.

Lemma weakening_env_declared_constructor :
  ∀ (H : checker_flags) (Σ : global_env) ind mdecl idecl decl,
    declared_constructor Σ ind mdecl idecl decl →
    ∀ Σ' : global_env, wf Σ' → extends Σ Σ' →
    declared_constructor Σ' ind mdecl idecl decl.

Lemma weakening_env_declared_projection :
  ∀ (H : checker_flags) (Σ : global_env) ind mdecl idecl decl,
    declared_projection Σ ind mdecl idecl decl →
    ∀ Σ' : global_env, wf Σ' → extends Σ Σ' →
    declared_projection Σ' ind mdecl idecl decl.

Lemma weakening_All_local_env_impl `{checker_flags}
      (P Q : context → term → option term → Type) l :
  All_local_env P l →
  (∀ Γ t T, P Γ t T → Q Γ t T) →
  All_local_env Q l.


Lemma weakening_env_consistent_instance {cf:checker_flags} Σ Σ' φ ctrs u (H : extends Σ Σ')
  : consistent_instance_ext (Σ, φ) ctrs u
    → consistent_instance_ext (Σ', φ) ctrs u.

Lemma weakening_env `{checker_flags} :
  env_prop (fun Σ Γ t T ⇒
              ∀ Σ', wf Σ' → extends Σ.1 Σ' → (Σ', Σ.2) ;;; Γ |- t : T).

Definition weaken_env_prop `{checker_flags}
           (P : global_env_ext → context → term → option term → Type) :=
  ∀ Σ Σ' φ, wf Σ' → extends Σ Σ' → ∀ Γ t T, P (Σ, φ) Γ t T → P (Σ', φ) Γ t T.

Lemma weakening_on_global_decl `{checker_flags} P Σ Σ' φ decl :
  weaken_env_prop P →
  wf Σ' → extends Σ Σ' →
  on_global_decl P (Σ, φ) decl →
  on_global_decl P (Σ', φ) decl.

Lemma weakening_env_lookup_on_global_env `{checker_flags} P Σ Σ' c decl :
  weaken_env_prop P →
  wf Σ' → extends Σ Σ' → on_global_env P Σ →
  lookup_env Σ c = Some decl →
  on_global_decl P (Σ', universes_decl_of_decl decl) decl.

Lemma weaken_lookup_on_global_env `{checker_flags} P Σ c decl :
  weaken_env_prop P →
  wf Σ → on_global_env P Σ →
  lookup_env Σ c = Some decl →
  on_global_decl P (Σ, universes_decl_of_decl decl) decl.

Lemma declared_constant_inv `{checker_flags} Σ P cst decl :
  weaken_env_prop (lift_typing P) →
  wf Σ → Forall_decls_typing P Σ →
  declared_constant Σ cst decl →
  on_constant_decl (lift_typing P) (Σ, cst_universes decl) decl.

Lemma declared_minductive_inv `{checker_flags} Σ P ind mdecl :
  weaken_env_prop (lift_typing P) →
  wf Σ → Forall_decls_typing P Σ →
  declared_minductive Σ ind mdecl →
  on_inductive (lift_typing P) (Σ, ind_universes mdecl) ind mdecl.

Lemma declared_inductive_inv `{checker_flags} Σ P ind mdecl idecl :
  weaken_env_prop (lift_typing P) →
  wf Σ → Forall_decls_typing P Σ →
  declared_inductive Σ mdecl ind idecl →
  on_ind_body (lift_typing P) (Σ, ind_universes mdecl) (inductive_mind ind) mdecl (inductive_ind ind) idecl.

Lemma declared_constructor_inv `{checker_flags} Σ P mdecl idecl ref cdecl :
  weaken_env_prop (lift_typing P) →
  wf Σ → Forall_decls_typing P Σ →
  declared_constructor Σ mdecl idecl ref cdecl →
  on_constructor (lift_typing P) (Σ, ind_universes mdecl) (inductive_mind (fst ref)) mdecl (inductive_ind (fst ref)) idecl (snd ref) cdecl.

Lemma declared_projection_inv `{checker_flags} Σ P mdecl idecl ref pdecl :
  weaken_env_prop (lift_typing P) →
  wf Σ → Forall_decls_typing P Σ →
  declared_projection Σ mdecl idecl ref pdecl →
  on_projection (lift_typing P) (Σ, ind_universes mdecl) (inductive_mind (fst (fst ref))) mdecl
                (inductive_ind (fst (fst ref))) idecl (snd ref) pdecl.

Lemma wf_extends `{checker_flags} {Σ Σ'} : wf Σ' → extends Σ Σ' → wf Σ.

Lemma weaken_env_prop_typing `{checker_flags} : weaken_env_prop (lift_typing typing).

Lemma weaken_wf_local `{checker_flags} (Σ : global_env_ext) Σ' Γ :
  extends Σ Σ' → wf Σ' → wf_local Σ Γ → wf_local (Σ', Σ.2) Γ.

Lemma on_declared_constant `{checker_flags} Σ cst decl :
  wf Σ → declared_constant Σ cst decl →
  on_constant_decl (lift_typing typing) (Σ, cst_universes decl) decl.

Lemma declared_constant_inj {Σ c} decl1 decl2 :
  declared_constant Σ c decl1 → declared_constant Σ c decl2 → decl1 = decl2.

Lemma on_declared_minductive `{checker_flags} {Σ ref decl} :
  wf Σ →
  declared_minductive Σ ref decl →
  on_inductive (lift_typing typing) (Σ, ind_universes decl) ref decl.

Lemma on_declared_inductive `{checker_flags} {Σ ref mdecl idecl} :
  wf Σ →
  declared_inductive Σ mdecl ref idecl →
  on_inductive (lift_typing typing) (Σ, ind_universes mdecl) (inductive_mind ref) mdecl ×
  on_ind_body (lift_typing typing) (Σ, ind_universes mdecl) (inductive_mind ref) mdecl (inductive_ind ref) idecl.

Lemma on_declared_constructor `{checker_flags} {Σ ref mdecl idecl cdecl} :
  wf Σ →
  declared_constructor Σ mdecl idecl ref cdecl →
  on_inductive (lift_typing typing) (Σ, ind_universes mdecl) (inductive_mind (fst ref)) mdecl ×
  on_ind_body (lift_typing typing) (Σ, ind_universes mdecl) (inductive_mind (fst ref)) mdecl (inductive_ind (fst ref)) idecl ×
  on_constructor (lift_typing typing) (Σ, ind_universes mdecl) (inductive_mind (fst ref)) mdecl (inductive_ind (fst ref)) idecl (snd ref) cdecl.

Lemma on_declared_projection `{checker_flags} {Σ ref mdecl idecl pdecl} :
  wf Σ →
  declared_projection Σ mdecl idecl ref pdecl →
  on_inductive (lift_typing typing) (Σ, ind_universes mdecl) (inductive_mind (fst (fst ref))) mdecl ×
  on_ind_body (lift_typing typing) (Σ, ind_universes mdecl) (inductive_mind (fst (fst ref))) mdecl (inductive_ind (fst (fst ref))) idecl ×
  on_projection (lift_typing typing) (Σ, ind_universes mdecl) (inductive_mind (fst (fst ref))) mdecl
                (inductive_ind (fst (fst ref))) idecl (snd ref) pdecl.

Definition on_udecl_prop `{checker_flags} Σ (udecl : universes_decl)
  := let levels := levels_of_udecl udecl in
     let global_levels := global_levels Σ in
     let all_levels := LevelSet.union levels global_levels in
     ConstraintSet.For_all (fun '(l1,_,l2) ⇒ LevelSet.In l1 all_levels
                                             ∧ LevelSet.In l2 all_levels)
                             (constraints_of_udecl udecl)
     ∧ match udecl with
       | Monomorphic_ctx ctx ⇒ LevelSet.for_all (negb ∘ Level.is_var) ctx.1
                               ∧ LevelSet.Subset ctx.1 global_levels
                               ∧ ConstraintSet.Subset ctx.2 (global_constraints Σ)
                               ∧ satisfiable_udecl Σ udecl
       | _ ⇒ True
       end.

Lemma weaken_lookup_on_global_env' `{checker_flags} Σ c decl :
  wf Σ →
  lookup_env Σ c = Some decl →
  on_udecl_prop Σ (universes_decl_of_decl decl).