Lemma typed_liftn `{checker_flags} Σ Γ t T n k :
  wf Σ.1 → wf_local Σ Γ → k ≥ #|Γ| →
  Σ ;;; Γ |- t : T → lift n k T = T ∧ lift n k t = t.

Definition lift_decl n k d := (map_decl (lift n k) d).

Definition lift_context n k (Γ : context) : context :=
  fold_context (fun k' ⇒ lift n (k' + k)) Γ.

Lemma lift_decl0 k d : map_decl (lift 0 k) d = d.

Lemma lift0_context k Γ : lift_context 0 k Γ = Γ.

Lemma lift_context_length n k Γ : #|lift_context n k Γ| = #|Γ|.

Definition lift_context_snoc0 n k Γ d : lift_context n k (d :: Γ) = lift_context n k Γ ,, lift_decl n (#|Γ| + k) d.

Lemma lift_context_snoc n k Γ d : lift_context n k (Γ ,, d) = lift_context n k Γ ,, lift_decl n (#|Γ| + k) d.

Lemma lift_context_alt n k Γ :
  lift_context n k Γ =
  mapi (fun k' d ⇒ lift_decl n (Nat.pred #|Γ| - k' + k) d) Γ.

Lemma lift_context_app n k Γ Δ :
  lift_context n k (Γ ,,, Δ) = lift_context n k Γ ,,, lift_context n (#|Γ| + k) Δ.

Lemma nth_error_lift_context:
  ∀ (Γ' Γ'' : context) (v : nat),
    v < #|Γ'| → ∀ nth k,
    nth_error Γ' v = Some nth →
    nth_error (lift_context #|Γ''| k Γ') v = Some (lift_decl #|Γ''| (#|Γ'| - S v + k) nth).

Lemma nth_error_lift_context_eq:
  ∀ (Γ' Γ'' : context) (v : nat) k,
    nth_error (lift_context #|Γ''| k Γ') v =
    option_map (lift_decl #|Γ''| (#|Γ'| - S v + k)) (nth_error Γ' v).

Lemma weaken_nth_error_ge {Γ Γ' v Γ''} : #|Γ'| ≤ v →
  nth_error (Γ ,,, Γ') v =
  nth_error (Γ ,,, Γ'' ,,, lift_context #|Γ''| 0 Γ') (#|Γ''| + v).

Lemma weaken_nth_error_lt {Γ Γ' Γ'' v} : v < #|Γ'| →
  nth_error (Γ ,,, Γ'' ,,, lift_context #|Γ''| 0 Γ') v =
  option_map (lift_decl #|Γ''| (#|Γ'| - S v)) (nth_error (Γ ,,, Γ') v).

Lemma lift_simpl {Γ'' Γ' : context} {i t} : i < #|Γ'| →
  lift0 (S i) (lift #|Γ''| (#|Γ'| - S i) t) = lift #|Γ''| #|Γ'| (lift0 (S i) t).

Lemma lift_iota_red n k pars c args brs :
  lift n k (iota_red pars c args brs) =
  iota_red pars c (List.map (lift n k) args) (List.map (on_snd (lift n k)) brs).

Lemma parsubst_empty k a : Ast.wf a → subst [] k a = a.

Lemma lift_unfold_fix n k mfix idx narg fn :
  unfold_fix mfix idx = Some (narg, fn) →
  unfold_fix (map (map_def (lift n k) (lift n (#|mfix| + k))) mfix) idx = Some (narg, lift n k fn).

Lemma lift_unfold_cofix n k mfix idx narg fn :
  unfold_cofix mfix idx = Some (narg, fn) →
  unfold_cofix (map (map_def (lift n k) (lift n (#|mfix| + k))) mfix) idx = Some (narg, lift n k fn).

Lemma lift_is_constructor:
  ∀ (args : list term) (narg : nat) n k,
    is_constructor narg args = true → is_constructor narg (map (lift n k) args) = true.


Lemma lift_declared_constant `{checker_flags} Σ cst decl n k :
  wf Σ →
  declared_constant Σ cst decl →
  decl = map_constant_body (lift n k) decl.

Definition lift_mutual_inductive_body n k m :=
  map_mutual_inductive_body (fun k' ⇒ lift n (k' + k)) m.

Lemma lift_wf_local `{checker_flags} Σ Γ n k : wf Σ.1 → wf_local Σ Γ → lift_context n k Γ = Γ.

Lemma closed_wf_local `{checker_flags} Σ Γ :
  wf Σ.1 →
  wf_local Σ Γ →
  closed_ctx Γ.

Lemma lift_declared_minductive `{checker_flags} Σ cst decl n k :
  wf Σ →
  declared_minductive Σ cst decl →
  lift_mutual_inductive_body n k decl = decl.

Lemma lift_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' ⇒ lift n (k' + k))
                         (inductive_ind ind) idecl = idecl.

Lemma subst0_inds_lift ind u mdecl n k t :
  (subst0 (inds (inductive_mind ind) u (ind_bodies mdecl))
          (lift n (#|arities_context (ind_bodies mdecl)| + k) t)) =
  lift n k (subst0 (inds (inductive_mind ind) u (ind_bodies mdecl)) t).

Lemma lift_declared_constructor `{checker_flags} Σ c u mdecl idecl cdecl n k :
  wf Σ →
  declared_constructor Σ mdecl idecl c cdecl →
  lift n k (type_of_constructor mdecl cdecl c u) = (type_of_constructor mdecl cdecl c u).

Lemma lift_declared_projection `{checker_flags} Σ c mdecl idecl pdecl n k :
  wf Σ →
  declared_projection Σ mdecl idecl c pdecl →
  on_snd (lift n (S (ind_npars mdecl + k))) pdecl = pdecl.

Lemma lift_fix_context:
  ∀ (mfix : list (def term)) (n k : nat),
    fix_context (map (map_def (lift n k) (lift n (#|mfix| + k))) mfix) = lift_context n k (fix_context mfix).


Lemma All_local_env_lift `{checker_flags}
      (P Q : context → term → option term → Type) c n k :
  All_local_env Q c →
  (∀ Γ t T,
      Q Γ t T →
      P (lift_context n k Γ) (lift n (#|Γ| + k) t)
        (option_map (lift n (#|Γ| + k)) T)
  ) →
  All_local_env P (lift_context n k c).

Lemma lift_destArity ctx t n k : Ast.wf t →
        destArity (lift_context n k ctx) (lift n (#|ctx| + k) t) =
        match destArity ctx t with
        | Some (args, s) ⇒ Some (lift_context n k args, s)
        | None ⇒ None
        end.

Lemma lift_strip_outer_cast n k t : lift n k (strip_outer_cast t) = strip_outer_cast (lift n k t).

Definition on_pair {A B C D} (f : A → B) (g : C → D) (x : A × C) :=
  (f (fst x), g (snd x)).

Lemma lift_instantiate_params_subst n k params args s t :
  instantiate_params_subst (mapi_rec (fun k' decl ⇒ lift_decl n (k' + k) decl) params #|s|)
                           (map (lift n k) args) (map (lift n k) s) (lift n (#|s| + k) t) =
  option_map (on_pair (map (lift n k)) (lift n (#|s| + k + #|params|))) (instantiate_params_subst params args s t).

Lemma instantiate_params_subst_length params args s t ctx t' :
  instantiate_params_subst params args s t = Some (ctx, t') →
  #|ctx| = #|s| + #|params|.

Lemma lift_decl_closed n k d : closed_decl k d → lift_decl n k d = d.

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

Lemma closed_ctx_lift n k ctx : closed_ctx ctx → lift_context n k ctx = ctx.

Lemma closed_tele_lift n k ctx :
  closed_ctx ctx →
  mapi (fun (k' : nat) (decl : context_decl) ⇒ lift_decl n (k' + k) decl) (List.rev ctx) = List.rev ctx.

Lemma lift_instantiate_params n k params args t :
  closed_ctx params →
  option_map (lift n k) (instantiate_params params args t) =
  instantiate_params params (map (lift n k) args) (lift n k t).

Lemma lift_decompose_prod_assum_rec ctx t n k :
  let (ctx', t') := decompose_prod_assum ctx t in
  (lift_context n k ctx', lift n (length ctx' + k) t') =
  decompose_prod_assum (lift_context n k ctx) (lift n (length ctx + k) t).

Lemma lift_decompose_prod_assum t n k :
  let (ctx', t') := decompose_prod_assum [] t in
  (lift_context n k ctx', lift n (length ctx' + k) t') =
  decompose_prod_assum [] (lift n k t).

Lemma decompose_app_lift n k t f a :
  decompose_app t = (f, a) → decompose_app (lift n k t) = (lift n k f, map (lift n k) a).

Lemma lift_it_mkProd_or_LetIn n k ctx t :
  lift n k (it_mkProd_or_LetIn ctx t) =
  it_mkProd_or_LetIn (lift_context n k ctx) (lift n (length ctx + k) t).

Lemma to_extended_list_lift n k c :
  to_extended_list (lift_context n k c) = to_extended_list c.

Lemma to_extended_list_map_lift:
  ∀ (n k : nat) (c : context), to_extended_list c = map (lift n (#|c| + k)) (to_extended_list c).

Lemma wf_instantiate_params_subst_term :
  ∀ params args s t ctx t',
    Ast.wf t →
    instantiate_params_subst params args s t = Some (ctx, t') →
    Ast.wf t'.

Lemma wf_instantiate_params_subst_ctx :
  ∀ params args s t ctx t',
    Forall Ast.wf args →
    Forall wf_decl params →
    Forall Ast.wf s →
    instantiate_params_subst params args s t = Some (ctx, t') →
    Forall Ast.wf ctx.

Lemma wf_instantiate_params :
  ∀ params args t t',
    Forall wf_decl params →
    Forall Ast.wf args →
    Ast.wf t →
    instantiate_params params args t = Some t' →
    Ast.wf t'.

Lemma lift_types_of_case ind mdecl idecl args u p pty indctx pctx ps btys n k :
  let f k' := lift n (k' + k) in
  let f_ctx := lift_context n k in
  Forall wf_decl mdecl.(ind_params) →
  Forall Ast.wf args →
  Ast.wf pty → Ast.wf (ind_type idecl) →
  closed_ctx mdecl.(ind_params) →
  types_of_case ind mdecl idecl args u p pty = Some (indctx, pctx, ps, btys) →
  types_of_case ind mdecl (map_one_inductive_body (context_assumptions mdecl.(ind_params))
                                                  (length (arities_context mdecl.(ind_bodies)))
                                                  f (inductive_ind ind) idecl)
                (map (f 0) args) u (f 0 p) (f 0 pty) =
  Some (f_ctx indctx, f_ctx pctx, ps, map (on_snd (f 0)) btys).

Lemma weakening_red1 `{CF:checker_flags} Σ Γ Γ' Γ'' M N :
  wf Σ →
  red1 Σ (Γ ,,, Γ') M N →
  red1 Σ (Γ ,,, Γ'' ,,, lift_context #|Γ''| 0 Γ') (lift #|Γ''| #|Γ'| M) (lift #|Γ''| #|Γ'| N).

Lemma lift_eq_term_upto_univ Re Rl n k T U :
  eq_term_upto_univ Re Rl T U →
  eq_term_upto_univ Re Rl (lift n k T) (lift n k U).

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

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

Lemma weakening_cumul `{CF:checker_flags} Σ Γ Γ' Γ'' M N :
  wf Σ.1 →
  Σ ;;; Γ ,,, Γ' |- M ≤ N →
  Σ ;;; Γ ,,, Γ'' ,,, lift_context #|Γ''| 0 Γ' |- lift #|Γ''| #|Γ'| M ≤ lift #|Γ''| #|Γ'| N.

Lemma lift_eq_decl `{checker_flags} ϕ n k d d' :
  eq_decl ϕ d d' → eq_decl ϕ (lift_decl n k d) (lift_decl n k d').

Lemma lift_eq_context `{checker_flags} φ l l' n k :
  eq_context φ l l' →
  eq_context φ (lift_context n k l) (lift_context n k l').

Lemma lift_check_correct_arity:
  ∀ (cf : checker_flags) φ (Γ' : context) (ind : inductive) (u : universe_instance)
         (npar : nat) (args : list term) (idecl : one_inductive_body)
         (Γ'' : context) (indctx pctx : list context_decl),
    check_correct_arity φ idecl ind u indctx (firstn npar args) pctx →
    check_correct_arity
      φ idecl ind u (lift_context #|Γ''| #|Γ'| indctx) (firstn npar (map (lift #|Γ''| #|Γ'|) args))
      (lift_context #|Γ''| #|Γ'| pctx).

Lemma wf_ind_type `{checker_flags} Σ mdecl ind idecl :
  wf Σ → declared_inductive Σ mdecl ind idecl → Ast.wf (ind_type idecl).

Lemma destArity_it_mkProd_or_LetIn ctx ctx' t :
  destArity ctx (it_mkProd_or_LetIn ctx' t) =
  destArity (ctx ,,, ctx') t.

Lemma weakening_typing `{cf : checker_flags} Σ Γ Γ' Γ'' (t : term) :
  wf Σ.1 →
  wf_local Σ (Γ ,,, Γ') →
  wf_local Σ (Γ ,,, Γ'' ,,, lift_context #|Γ''| 0 Γ') →
  `(Σ ;;; Γ ,,, Γ' |- t : T →
    Σ ;;; Γ ,,, Γ'' ,,, lift_context #|Γ''| 0 Γ' |-
    lift #|Γ''| #|Γ'| t : lift #|Γ''| #|Γ'| T).

Lemma weakening `{cf : checker_flags} Σ Γ Γ' (t : term) T :
  wf Σ.1 → wf_local Σ (Γ ,,, Γ') →
  Σ ;;; Γ |- t : T →
  Σ ;;; Γ ,,, Γ' |- lift0 #|Γ'| t : lift0 #|Γ'| T.