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

Definition closed_ctx ctx :=
  forallb id (mapi (fun k d ⇒ closed_decl k d) (List.rev 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 : Ast.wf t →
  closedn k t → subst s k t = t.

Lemma closedn_subst_instance_constr k t u :
  closedn k (UnivSubst.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.

Definition closedn_ctx n ctx :=
  forallb id (mapi (fun k d ⇒ closed_decl (n + k) d) (List.rev 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_All_local_closed:
  ∀ (cf : checker_flags) (Σ : global_env_ext) (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 ctx.

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 declared_decl_closed `{checker_flags} (Σ : global_env) cst decl :
  wf Σ →
  lookup_env Σ cst = Some decl →
  on_global_decl (fun Σ Γ b t ⇒
                    match t with Some t ⇒ Ast.wf t | None ⇒ True end ∧ Ast.wf b ∧
                    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.