Definition wf_decl d :=
  match decl_body d with
  | Some b ⇒ Ast.wf b
  | None ⇒ True
  end ∧ Ast.wf (decl_type d).

Definition wf_decl_pred : context → term → option term → Type :=
  (fun _ t T ⇒ Ast.wf t ∧ match T with
                        | Some T ⇒ Ast.wf T
                        | None ⇒ True
                        end).

Lemma All_local_env_wf_decl :
  ∀ (Γ : context),
    Forall wf_decl Γ → All_local_env wf_decl_pred Γ.

Lemma All_local_env_wf_decl_inv:
  ∀ (a : context_decl) (Γ : list context_decl)
         (X : All_local_env wf_decl_pred (a :: Γ)),
    on_local_decl wf_decl_pred Γ a × All_local_env wf_decl_pred Γ.

Lemma wf_strip_outer_cast t : Ast.wf t → Ast.wf (strip_outer_cast t).

Lemma wf_mkApps_napp t u : isApp t = false → Ast.wf (mkApps t u) → Ast.wf t ∧ List.Forall Ast.wf u.

Lemma wf_mkApps_inv t u : Ast.wf (mkApps t u) → List.Forall Ast.wf u.

Lemma isLambda_isApp t : isLambda t = true → isApp t = false.

Lemma unfold_fix_wf:
  ∀ (mfix : mfixpoint term) (idx : nat) (narg : nat) (fn : term),
    unfold_fix mfix idx = Some (narg, fn) →
    Ast.wf (tFix mfix idx) →
    Ast.wf fn ∧ isApp fn = false.

Lemma unfold_cofix_wf:
  ∀ (mfix : mfixpoint term) (idx : nat) (narg : nat) (fn : term),
    unfold_cofix mfix idx = Some (narg, fn) →
    Ast.wf (tCoFix mfix idx) → Ast.wf fn.

Lemma wf_subst_instance_constr u c :
  Ast.wf c → Ast.wf (subst_instance_constr u c).

Lemma wf_nth:
  ∀ (n : nat) (args : list term), Forall Ast.wf args → Ast.wf (nth n args tDummy).

Lemma red1_isLambda Σ Γ t u :
  red1 Σ Γ t u → isLambda t → isLambda u.

Lemma OnOne2_All_All {A} {P Q} {l l' : list A} :
  OnOne2 P l l' →
  (∀ x y, P x y → Q x → Q y) →
  All Q l → All Q l'.

Lemma All_mapi {A B} (P : B → Type) (l : list A) (f : nat → A → B) :
  Alli (fun i x ⇒ P (f i x)) 0 l → All P (mapi f l).

Lemma Alli_id {A} (P : nat → A → Type) n (l : list A) :
  (∀ n x, P n x) → Alli P n l.

Lemma All_Alli {A} {P : A → Type} {Q : nat → A → Type} {l n} :
  All P l →
  (∀ n x, P x → Q n x) →
  Alli Q n l.

Lemma wf_red1 {cf:checker_flags} Σ Γ M N :
  on_global_env (fun Σ ⇒ wf_decl_pred) Σ →
  List.Forall wf_decl Γ →
  Ast.wf M → red1 Σ Γ M N → Ast.wf N.


Lemma wf_inds mind bodies u : Forall Ast.wf (inds mind u bodies).



Lemma wf_lift_wf n k t : Ast.wf (lift n k t) → Ast.wf t.

Lemma declared_projection_wf {cf:checker_flags}:
  ∀ (Σ : global_env) (p : projection) (u : universe_instance)
         (mdecl : mutual_inductive_body) (idecl : one_inductive_body) (pdecl : ident × term),
    declared_projection Σ mdecl idecl p pdecl →
    Forall_decls_typing (fun (_ : global_env_ext) (_ : context) (t T : term) ⇒ Ast.wf t ∧ Ast.wf T) Σ →
    Ast.wf (subst_instance_constr u (snd pdecl)).

Lemma declared_inductive_wf {cf:checker_flags} :
  ∀ (Σ : global_env) ind
         (mdecl : mutual_inductive_body) (idecl : one_inductive_body),
  Forall_decls_typing (fun (_ : global_env_ext) (_ : context) (t T : term) ⇒ Ast.wf t ∧ Ast.wf T) Σ →
  declared_inductive Σ mdecl ind idecl → Ast.wf (ind_type idecl).

Lemma declared_constructor_wf {cf:checker_flags}:
  ∀ (Σ : global_env) (ind : inductive) (i : nat) (u : list Level.t)
         (mdecl : mutual_inductive_body) (idecl : one_inductive_body) (cdecl : ident × term × nat),
    Forall_decls_typing (fun (_ : global_env_ext) (_ : context) (t T : term) ⇒ Ast.wf t ∧ Ast.wf T) Σ →
    declared_constructor Σ mdecl idecl (ind, i) cdecl →
    Ast.wf (snd (fst cdecl)).

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 wf_it_mkProd_or_LetIn `{checker_flags} Σ Γ (wfΓ : wf_local Σ Γ)
  : All_local_env_over typing
  (fun (Σ : global_env_ext) (Γ : context) (_ : wf_local Σ Γ)
     (t T : term) (_ : Σ;;; Γ |- t : T) ⇒ Ast.wf t ∧ Ast.wf T) Σ
         Γ wfΓ
→ ∀ t, Ast.wf t → Ast.wf (it_mkProd_or_LetIn Γ t).

Lemma it_mkProd_or_LetIn_wf Γ t
  : Ast.wf (it_mkProd_or_LetIn Γ t) → Ast.wf t.

Lemma typing_wf_gen {cf:checker_flags} : env_prop (fun Σ Γ t T ⇒ Ast.wf t ∧ Ast.wf T).

Lemma typing_all_wf_decl {cf:checker_flags} Σ (wfΣ : wf Σ.1) Γ (wfΓ : wf_local Σ Γ) :
  Forall wf_decl Γ.

Lemma typing_wf_sigma {cf:checker_flags} Σ (wfΣ : wf Σ) :
  on_global_env (fun _ ⇒ wf_decl_pred) Σ.

Lemma typing_wf {cf:checker_flags} Σ (wfΣ : wf Σ.1) Γ t T :
  Σ ;;; Γ |- t : T → Ast.wf t ∧ Ast.wf T.