Definition closed_decl n d :=
  option_default (closedn n) d.(decl_body) true && closedn n d.(decl_type).

Definition closedn_ctx n ctx :=
  forallb id (mapi (fun k d ⇒ closed_decl (n + k) d) (List.rev ctx)).

Notation closed_ctx ctx := (closedn_ctx 0 ctx).

Lemma closedn_lift n k k' t : closedn k t → closedn (k + n) (lift n k' t).

Lemma closedn_lift_inv n k k' t : k ≤ k' →
                                   closedn (k' + n) (lift n k t) →
                                   closedn k' t.

Lemma closedn_mkApps k f u:
  closedn k f → forallb (closedn k) u →
  closedn k (mkApps f u).

Lemma closedn_mkApps_inv k f u:
  closedn k (mkApps f u) →
  closedn k f && forallb (closedn k) u.

Lemma closedn_subst s k k' t :
  forallb (closedn k) s → closedn (k + k' + #|s|) t →
  closedn (k + k') (subst s k' t).

Lemma closedn_subst0 s k t :
  forallb (closedn k) s → closedn (k + #|s|) t →
  closedn k (subst0 s t).

Lemma subst_closedn s k t : closedn k t → subst s k t = t.


    Instance Upn_ext n : Proper (`=1` ==> `=1`) (Upn n).

    Instance Up_ext : Proper (`=1` ==> `=1`) Up.

    Lemma Upn_S σ n : ⇑^(S n) σ =1 ⇑ ⇑^n σ.


Instance up_proper k : Proper (`=1` ==> `=1`) (up k).

Lemma Upn_Upn k k' σ : ⇑^(k + k') σ =1 ⇑^k (⇑^k' σ).

Lemma inst_closed σ k t : closedn k t → t.[⇑^k σ] = t.

Lemma All_forallb_eq_forallb {A} (P : A → Type) (p q : A → bool) l :
  All P l →
  (∀ x, P x → p x = q x) →
  forallb p l = forallb q l.

Lemma closedn_subst_instance_constr k t u :
  closedn k (subst_instance_constr u t) = closedn k t.


Lemma destArity_spec ctx T :
  match destArity ctx T with
  | Some (ctx', s) ⇒ it_mkProd_or_LetIn ctx T = it_mkProd_or_LetIn ctx' (tSort s)
  | None ⇒ True
  end.

Lemma closedn_All_local_closed:
  ∀ (cf : checker_flags) (Σ : global_env_ext) (Γ : context) (ctx : list context_decl)
         (wfΓ' : wf_local Σ (Γ ,,, ctx)),
    All_local_env_over typing
    (fun (Σ0 : global_env_ext) (Γ0 : context) (_ : wf_local Σ0 Γ0) (t T : term) (_ : Σ0;;; Γ0 |- t : T) ⇒
       closedn #|Γ0| t && closedn #|Γ0| T) Σ (Γ ,,, ctx) wfΓ' →
    closedn_ctx 0 Γ && closedn_ctx #|Γ| ctx.

Lemma closedn_ctx_cons n d Γ : closedn_ctx n (d :: Γ) → closedn_ctx n Γ && closed_decl (n + #|Γ|) d.

Lemma closedn_ctx_app n Γ Γ' :
  closedn_ctx n (Γ ,,, Γ') =
  closedn_ctx n Γ && closedn_ctx (n + #|Γ|) Γ'.

Lemma closedn_mkProd_or_LetIn (Γ : context) d T :
    closed_decl #|Γ| d →
    closedn (S #|Γ|) T → closedn #|Γ| (mkProd_or_LetIn d T).

Lemma closedn_mkLambda_or_LetIn (Γ : context) d T :
    closed_decl #|Γ| d →
    closedn (S #|Γ|) T → closedn #|Γ| (mkLambda_or_LetIn d T).

Lemma closedn_it_mkProd_or_LetIn
      (Γ : context) (ctx : list context_decl) T :
    closedn_ctx #|Γ| ctx →
    closedn (#|Γ| + #|ctx|) T → closedn #|Γ| (it_mkProd_or_LetIn ctx T).

Lemma closedn_it_mkLambda_or_LetIn
      (Γ : context) (ctx : list context_decl) T :
    closedn_ctx #|Γ| ctx →
    closedn (#|Γ| + #|ctx|) T → closedn #|Γ| (it_mkLambda_or_LetIn ctx T).

Lemma typecheck_closed `{cf : checker_flags} :
  env_prop (fun Σ Γ t T ⇒
              closedn #|Γ| t && closedn #|Γ| T).

Lemma on_global_env_impl `{checker_flags} Σ P Q :
  (∀ Σ Γ t T, on_global_env P Σ.1 → P Σ Γ t T → Q Σ Γ t T) →
  on_global_env P Σ → on_global_env Q Σ.

Lemma declared_decl_closed `{checker_flags} (Σ : global_env) cst decl :
  wf Σ →
  lookup_env Σ cst = Some decl →
  on_global_decl (fun Σ Γ b t ⇒ closedn #|Γ| b && option_default (closedn #|Γ|) t true)
                 (Σ, universes_decl_of_decl decl) decl.

Lemma closed_decl_upwards k d : closed_decl k d → ∀ k', k ≤ k' → closed_decl k' d.

Lemma rev_subst_instance_context u Γ :
  List.rev (subst_instance_context u Γ) = subst_instance_context u (List.rev Γ).

Lemma closedn_subst_instance_context k Γ u :
  closedn_ctx k (subst_instance_context u Γ) = closedn_ctx k Γ.