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

Definition subst_context n k (Γ : context) : context :=
  fold_context (fun k' ⇒ subst n (k' + k)) Γ.

Inductive subs `{cf : checker_flags} Σ (Γ : 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.

Lemma subst_decl0 Γ k d : on_local_decl wf_decl_pred Γ d → map_decl (subst [] k) d = d.

Lemma subst0_context k Γ : All_local_env wf_decl_pred Γ → 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 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 (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 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 subst_length `{checker_flags} Σ Γ s Γ' : subs Σ Γ s Γ' → #|s| = #|Γ'|.


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

Lemma subs_nth_error_lt `{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 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 :
  All Ast.wf n →
  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 :
  All Ast.wf n →
  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 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 (UnivSubst.subst_instance_constr u) decl) =
  map_constant_body (UnivSubst.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 `{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 :
  All Ast.wf n →
  (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 Σ → All Ast.wf n →
  declared_constructor Σ mdecl idecl c cdecl →
  subst (map (UnivSubst.subst_instance_constr u) n) k (type_of_constructor mdecl cdecl c u) = (type_of_constructor mdecl cdecl c u).

Lemma subst_declared_projection `{checker_flags} Σ c mdecl idecl pdecl n k :
  wf Σ → All Ast.wf n →
  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 :
  Ast.wf t →
  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).

Definition strip_outer_cast_tProd_tLetIn_morph f :=
  ∀ t k,
  match strip_outer_cast t with
  | tProd na A B ⇒
    strip_outer_cast (f k t) = tProd na (f k A) (f (S k) B)
  | tLetIn na b ty b' ⇒
    strip_outer_cast (f k t) = tLetIn na (f k b) (f k ty) (f (S k) b')
  | _ ⇒ True
  end.

Lemma strip_outer_cast_tProd_tLetIn_subst n :
  strip_outer_cast_tProd_tLetIn_morph (subst n).

Lemma strip_outer_cast_subst_instance_constr u t :
  strip_outer_cast (subst_instance_constr u t) =
  subst_instance_constr u (strip_outer_cast t).

Lemma strip_outer_cast_tProd_tLetIn_subst_instance_constr u :
  strip_outer_cast_tProd_tLetIn_morph (fun _ ⇒ subst_instance_constr u).

Lemma subst_instantiate_params_subst n k params args s t :
  All Ast.wf n → ∀ 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 : wf_decl d → closed_decl k d → subst_decl n k d = d.

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

Lemma closed_tele_subst n k ctx :
  All wf_decl 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 :
  All wf_decl params → All Ast.wf n → All Ast.wf args → Ast.wf t →
  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 `{checker_flags} Σ mind mdecl : wf Σ →
  declared_minductive Σ mind mdecl → wf_local (Σ, ind_universes mdecl) (arities_context mdecl.(ind_bodies)).

Lemma on_constructor_closed_wf `{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 = true ∧ Ast.wf cty.

Lemma on_projection_closed_wf `{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 = true ∧ Ast.wf 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 :
  All Ast.wf s →
  make_context_subst (List.rev ctx) args [] = Some s →
  map (subst s k) (to_extended_list_k ctx k) = map (lift0 k) args.

Lemma wf_context_subst ctx args s :
  All wf_decl ctx → All Ast.wf args →
  context_subst ctx args s → All Ast.wf s.

Lemma wf_make_context_subst ctx args s' :
  All wf_decl ctx → All Ast.wf args →
  make_context_subst (List.rev ctx) args [] = Some s' → All Ast.wf s'.


Lemma subst_types_of_case `{CF:checker_flags} Σ 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 Σ →
  All Ast.wf n → All Ast.wf args →
  Ast.wf pty → Ast.wf (ind_type idecl) →
  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).


Lemma subs_nth_error `{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 red1_tApp_mkApps_l Σ Γ M1 N1 M2 :
  red1 Σ Γ M1 N1 → red1 Σ Γ (tApp M1 M2) (mkApps N1 M2).

Lemma red1_tApp_mkApp Σ Γ M1 N1 M2 :
  red1 Σ Γ M1 N1 → red1 Σ Γ (tApp M1 [M2]) (mkApp N1 M2).

Lemma red1_mkApp Σ Γ M1 N1 M2 :
  Ast.wf M1 →
  red1 Σ Γ M1 N1 → red1 Σ Γ (mkApp M1 M2) (mkApp N1 M2).

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

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

Lemma wf_fix :
  ∀ (mfix : list (def term)) (k : nat), Ast.wf (tFix mfix k) →
    Forall
      (fun def : def term ⇒ Ast.wf (dtype def) ∧ Ast.wf (dbody def) ∧ isLambda (dbody def) = true)
      mfix.

Lemma wf_cofix :
  ∀ (mfix : list (def term)) (k : nat), Ast.wf (tCoFix mfix k) →
    Forall
      (fun def : def term ⇒ Ast.wf (dtype def) ∧ Ast.wf (dbody def))
      mfix.

Lemma substitution_red1 `{CF:checker_flags} Σ Γ Γ' Γ'' s M N :
  wf Σ.1 → All Ast.wf s → subs Σ Γ s Γ' → wf_local Σ Γ → Ast.wf M →
  red1 (fst Σ) (Γ ,,, Γ' ,,, Γ'') M N →
  red1 (fst Σ) (Γ ,,, subst_context s 0 Γ'') (subst s #|Γ''| M) (subst s #|Γ''| N).

Lemma eq_term_upto_univ_refl Re Rle :
  RelationClasses.Reflexive Re →
  RelationClasses.Reflexive Rle →
  ∀ t, eq_term_upto_univ Re Rle t t.

Lemma eq_term_refl `{checker_flags} φ t : eq_term φ t t.

Lemma leq_term_refl `{checker_flags} φ t : leq_term φ t t.

Lemma eq_term_leq_term `{checker_flags} φ t u : eq_term φ t u → leq_term φ t u.

Lemma eq_term_upto_univ_App `{checker_flags} Re Rle f f' :
  eq_term_upto_univ Re Rle f f' →
  isApp f = isApp f'.

Lemma eq_term_App `{checker_flags} φ f f' :
  eq_term φ f f' →
  isApp f = isApp f'.

Lemma eq_term_upto_univ_mkApps `{checker_flags} Re Rle f l f' l' :
  eq_term_upto_univ Re Rle f f' →
  Forall2 (eq_term_upto_univ Re Re) l l' →
  eq_term_upto_univ Re Rle (mkApps f l) (mkApps f' l').

Lemma leq_term_mkApps `{checker_flags} φ f l f' l' :
  leq_term φ f f' →
  Forall2 (eq_term φ) l l' →
  leq_term φ (mkApps f l) (mkApps f' l').

Lemma leq_term_App `{checker_flags} φ f f' :
  leq_term φ f f' →
  isApp f = isApp f'.

Lemma subst_eq_term_upto_univ `{checker_flags} Re Rle n k T U :
  RelationClasses.Reflexive Re →
  RelationClasses.Reflexive Rle →
  eq_term_upto_univ Re Rle T U →
  eq_term_upto_univ Re Rle (subst n k T) (subst n k U).

Lemma subst_eq_term `{checker_flags} ϕ n k T U :
  eq_term ϕ T U →
  eq_term ϕ (subst n k T) (subst n k U).

Lemma subst_leq_term `{checker_flags} ϕ n k T U :
  leq_term ϕ T U →
  leq_term ϕ (subst n k T) (subst n k U).

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 subs_wf `{checker_flags} Σ Γ s Δ : wf Σ.1 → subs Σ Γ s Δ → All Ast.wf s.

Lemma wf_red1_wf `{checker_flags} Σ Γ M N : wf Σ.1 → wf_local Σ Γ → Ast.wf M → red1 (fst Σ) Γ M N → Ast.wf N.

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

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

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

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