Lemma subst1_inst :
  ∀ t n u,
    t{ n := u } = t.[⇑^n (u ⋅ ids)].

Lemma rename_mkApps :
  ∀ f t l,
    rename f (mkApps t l) = mkApps (rename f t) (map (rename f) l).

Lemma rename_subst_instance_constr :
  ∀ u t f,
    rename f (subst_instance_constr u t) = subst_instance_constr u (rename f t).

Definition rename_context f (Γ : context) : context :=
  fold_context (fun i ⇒ rename (shiftn i f)) Γ.

Lemma rename_context_length :
  ∀ σ Γ,
    #|rename_context σ Γ| = #|Γ|.

Definition rename_decl f d :=
  map_decl (rename f) d.

Lemma rename_context_snoc :
  ∀ f Γ d,
    rename_context f (d :: Γ) =
    rename_context f Γ ,, rename_decl (shiftn #|Γ| f) d.

Definition inst_context σ (Γ : context) : context :=
  fold_context (fun i ⇒ inst (⇑^i σ)) Γ.

Lemma inst_context_length :
  ∀ σ Γ,
    #|inst_context σ Γ| = #|Γ|.

Definition inst_decl σ d :=
  map_decl (inst σ) d.

Lemma inst_context_snoc :
  ∀ σ Γ d,
    inst_context σ (d :: Γ) =
    inst_context σ Γ ,, inst_decl (⇑^#|Γ| σ) d.

Lemma rename_decl_inst_decl :
  ∀ f d,
    rename_decl f d = inst_decl (ren f) d.

Lemma rename_context_inst_context :
  ∀ f Γ,
    rename_context f Γ = inst_context (ren f) Γ.


Lemma rename_subst0 :
  ∀ f l t,
    rename f (subst0 l t) =
    subst0 (map (rename f) l) (rename (shiftn #|l| f) t).

Lemma rename_subst10 :
  ∀ f t u,
    rename f (t{ 0 := u }) = (rename (shiftn 1 f) t){ 0 := rename f u }.

Lemma rename_context_nth_error :
  ∀ f Γ i decl,
    nth_error Γ i = Some decl →
    nth_error (rename_context f Γ) i =
    Some (rename_decl (shiftn (#|Γ| - S i) f) decl).

Lemma rename_context_decl_body :
  ∀ f Γ i body,
    option_map decl_body (nth_error Γ i) = Some (Some body) →
    option_map decl_body (nth_error (rename_context f Γ) i) =
    Some (Some (rename (shiftn (#|Γ| - S i) f) body)).



Section Renaming.

Context `{checker_flags}.

Lemma eq_term_upto_univ_rename :
  ∀ Re Rle u v f,
    eq_term_upto_univ Re Rle u v →
    eq_term_upto_univ Re Rle (rename f u) (rename f v).

Definition urenaming Γ Δ f :=
  ∀ i decl,
    nth_error Δ i = Some decl →
    ∑ decl',
      nth_error Γ (f i) = Some decl' ×
      rename f (lift0 (S i) decl.(decl_type))
      = lift0 (S (f i)) decl'.(decl_type) ×
      (∀ b,
         decl.(decl_body) = Some b →
         ∑ b',
           decl'.(decl_body) = Some b' ×
           rename f (lift0 (S i) b) = lift0 (S (f i)) b'
      ).

Definition renaming Σ Γ Δ f :=
  wf_local Σ Γ × urenaming Γ Δ f.

Lemma rename_iota_red :
  ∀ f pars c args brs,
    rename f (iota_red pars c args brs) =
    iota_red pars c (map (rename f) args) (map (on_snd (rename f)) brs).

Lemma isLambda_rename :
  ∀ t f,
    isLambda t →
    isLambda (rename f t).

Lemma rename_unfold_fix :
  ∀ mfix idx narg fn f,
    unfold_fix mfix idx = Some (narg, fn) →
    unfold_fix (map (map_def (rename f) (rename (shiftn #|mfix| f))) mfix) idx
    = Some (narg, rename f fn).

Lemma decompose_app_rename :
  ∀ f t u l,
    decompose_app t = (u, l) →
    decompose_app (rename f t) = (rename f u, map (rename f) l).

Lemma isConstruct_app_rename :
  ∀ t f,
    isConstruct_app t →
    isConstruct_app (rename f t).

Lemma is_constructor_rename :
  ∀ n l f,
    is_constructor n l →
    is_constructor n (map (rename f) l).

Lemma rename_unfold_cofix :
  ∀ mfix idx narg fn f,
    unfold_cofix mfix idx = Some (narg, fn) →
    unfold_cofix (map (map_def (rename f) (rename (shiftn #|mfix| f))) mfix) idx
    = Some (narg, rename f fn).

Lemma rename_closedn :
  ∀ f n t,
    closedn n t →
    rename (shiftn n f) t = t.

Lemma rename_closed :
  ∀ f t,
    closed t →
    rename f t = t.

Lemma declared_constant_closed_body :
  ∀ Σ cst decl body,
    wf Σ →
    declared_constant Σ cst decl →
    decl.(cst_body) = Some body →
    closed body.

Lemma rename_shiftn :
  ∀ f t,
    rename (shiftn 1 f) (lift0 1 t) = lift0 1 (rename f t).

Lemma urenaming_vass :
  ∀ Γ Δ na A f,
    urenaming Γ Δ f →
    urenaming (Γ ,, vass na (rename f A)) (Δ ,, vass na A) (shiftn 1 f).

Lemma renaming_vass :
  ∀ Σ Γ Δ na A f,
    wf_local Σ (Γ ,, vass na (rename f A)) →
    renaming Σ Γ Δ f →
    renaming Σ (Γ ,, vass na (rename f A)) (Δ ,, vass na A) (shiftn 1 f).

Lemma urenaming_vdef :
  ∀ Γ Δ na b B f,
    urenaming Γ Δ f →
    urenaming (Γ ,, vdef na (rename f b) (rename f B)) (Δ ,, vdef na b B) (shiftn 1 f).

Lemma renaming_vdef :
  ∀ Σ Γ Δ na b B f,
    wf_local Σ (Γ ,, vdef na (rename f b) (rename f B)) →
    renaming Σ Γ Δ f →
    renaming Σ (Γ ,, vdef na (rename f b) (rename f B)) (Δ ,, vdef na b B) (shiftn 1 f).

Lemma urenaming_ext :
  ∀ Γ Δ f g,
    f =1 g →
    urenaming Δ Γ f →
    urenaming Δ Γ g.

Lemma urenaming_context :
  ∀ Γ Δ Ξ f,
    urenaming Δ Γ f →
    urenaming (Δ ,,, rename_context f Ξ) (Γ ,,, Ξ) (shiftn #|Ξ| f).

Lemma rename_fix_context :
  ∀ f mfix,
    rename_context f (fix_context mfix) =
    fix_context (map (map_def (rename f) (rename (shiftn #|mfix| f))) mfix).


Lemma red1_rename :
  ∀ Σ Γ Δ u v f,
    wf Σ →
    urenaming Δ Γ f →
    red1 Σ Γ u v →
    red1 Σ Δ (rename f u) (rename f v).

Lemma meta_conv :
  ∀ Σ Γ t A B,
    Σ ;;; Γ |- t : A →
    A = B →
    Σ ;;; Γ |- t : B.

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

Lemma instantiate_params_subst_inst :
  ∀ params pars s t σ s' t',
    instantiate_params_subst params pars s t = Some (s', t') →
    instantiate_params_subst
      (mapi_rec (fun i decl ⇒ inst_decl (⇑^i σ) decl) params #|s|)
      (map (inst σ) pars)
      (map (inst σ) s)
      t.[⇑^#|s| σ]
    = Some (map (inst σ) s', t'.[⇑^(#|s| + #|params|) σ]).

Lemma inst_decl_closed :
  ∀ σ k d,
    closed_decl k d →
    inst_decl (⇑^k σ) d = d.

Lemma closed_tele_inst :
  ∀ σ ctx,
    closed_ctx ctx →
    mapi (fun i decl ⇒ inst_decl (⇑^i σ) decl) (List.rev ctx) =
    List.rev ctx.

Lemma instantiate_params_inst :
  ∀ params pars T σ T',
    closed_ctx params →
    instantiate_params params pars T = Some T' →
    instantiate_params params (map (inst σ) pars) T.[σ] = Some T'.[σ].

Corollary instantiate_params_rename :
  ∀ params pars T f T',
    closed_ctx params →
    instantiate_params params pars T = Some T' →
    instantiate_params params (map (rename f) pars) (rename f T) =
    Some (rename f T').

Lemma build_branches_type_rename :
  ∀ ind mdecl idecl args u p brs f,
    closed_ctx (subst_instance_context u (ind_params mdecl)) →
    map_option_out (build_branches_type ind mdecl idecl args u p) = Some brs →
    map_option_out (
        build_branches_type
          ind
          mdecl
          (map_one_inductive_body
             (context_assumptions (ind_params mdecl))
             #|arities_context (ind_bodies mdecl)|
             (fun i : nat ⇒ rename (shiftn i f))
             (inductive_ind ind)
             idecl
          )
          (map (rename f) args)
          u
          (rename f p)
    ) = Some (map (on_snd (rename f)) brs).

Lemma typed_inst :
  ∀ Σ Γ t T k σ,
    wf Σ.1 →
    k ≥ #|Γ| →
    Σ ;;; Γ |- t : T →
    T.[⇑^k σ] = T ∧ t.[⇑^k σ] = t.

Lemma inst_wf_local :
  ∀ Σ Γ σ,
    wf Σ.1 →
    wf_local Σ Γ →
    inst_context σ Γ = Γ.

Definition inst_mutual_inductive_body σ m :=
  map_mutual_inductive_body (fun i ⇒ inst (⇑^i σ)) m.

Lemma inst_declared_minductive :
  ∀ Σ cst decl σ,
    wf Σ →
    declared_minductive Σ cst decl →
    inst_mutual_inductive_body σ decl = decl.

Lemma inst_declared_inductive :
  ∀ Σ ind mdecl idecl σ,
    wf Σ →
    declared_inductive Σ mdecl ind idecl →
    map_one_inductive_body
      (context_assumptions mdecl.(ind_params))
      #|arities_context mdecl.(ind_bodies)|
      (fun i ⇒ inst (⇑^i σ))
      ind.(inductive_ind)
      idecl
    = idecl.

Lemma inst_destArity :
  ∀ ctx t σ args s,
    destArity ctx t = Some (args, s) →
    destArity (inst_context σ ctx) t.[⇑^#|ctx| σ] =
    Some (inst_context σ args, s).

Lemma types_of_case_rename :
  ∀ Σ ind mdecl idecl npar args u p pty indctx pctx ps btys f,
    wf Σ →
    declared_inductive Σ mdecl ind idecl →
    types_of_case ind mdecl idecl (firstn npar args) u p pty =
    Some (indctx, pctx, ps, btys) →
    types_of_case
      ind mdecl idecl
      (firstn npar (map (rename f) args)) u (rename f p) (rename f pty)
    =
    Some (
        rename_context f indctx,
        rename_context f pctx,
        ps,
        map (on_snd (rename f)) btys
    ).

Lemma declared_constant_closed_type :
  ∀ Σ cst decl,
    wf Σ →
    declared_constant Σ cst decl →
    closed decl.(cst_type).

Lemma declared_inductive_closed_type :
  ∀ Σ mdecl ind idecl,
    wf Σ →
    declared_inductive Σ mdecl ind idecl →
    closed idecl.(ind_type).

Lemma declared_inductive_closed_constructors :
  ∀ Σ ind mdecl idecl,
      wf Σ →
      declared_inductive Σ mdecl ind idecl →
      All (fun '(na, t, n) ⇒ closedn #|arities_context mdecl.(ind_bodies)| t)
          idecl.(ind_ctors).

Lemma declared_minductive_closed_inds :
  ∀ Σ ind mdecl u,
    wf Σ →
    declared_minductive Σ (inductive_mind ind) mdecl →
    forallb (closedn 0) (inds (inductive_mind ind) u (ind_bodies mdecl)).

Lemma declared_inductive_closed_inds :
  ∀ Σ ind mdecl idecl u,
      wf Σ →
      declared_inductive Σ mdecl ind idecl →
      forallb (closedn 0) (inds (inductive_mind ind) u (ind_bodies mdecl)).

Lemma declared_constructor_closed_type :
  ∀ Σ mdecl idecl c cdecl u,
    wf Σ →
    declared_constructor Σ mdecl idecl c cdecl →
    closed (type_of_constructor mdecl cdecl c u).

Lemma declared_projection_closed_type :
  ∀ Σ mdecl idecl p pdecl,
    wf Σ →
    declared_projection Σ mdecl idecl p pdecl →
    closedn (S (ind_npars mdecl)) pdecl.2.

Lemma cumul_rename :
  ∀ Σ Γ Δ f A B,
    wf Σ.1 →
    renaming Σ Δ Γ f →
    Σ ;;; Γ |- A ≤ B →
    Σ ;;; Δ |- rename f A ≤ rename f B.

Lemma typing_rename :
  ∀ Σ Γ Δ f t A,
    wf Σ.1 →
    wf_local Σ Γ →
    renaming Σ Δ Γ f →
    Σ ;;; Γ |- t : A →
    Σ ;;; Δ |- rename f t : rename f A.

End Renaming.

Section Sigma.

Context `{checker_flags}.


Definition well_subst Σ (Γ : context) σ (Δ : context) :=
  ∀ x decl,
    nth_error Γ x = Some decl →
    Σ ;;; Δ |- σ x : ((lift0 (S x)) (decl_type decl)).[ σ ] ×
    (∀ b,
        decl.(decl_body) = Some b →
        σ x = b.[⇑^(S x) σ]
    ).

Notation "Σ ;;; Δ ⊢ σ : Γ" :=
  (well_subst Σ Γ σ Δ) (at level 50, Δ, σ, Γ at next level).

Lemma well_subst_Up :
  ∀ Σ Γ Δ σ na A,
    wf_local Σ (Δ ,, vass na A.[σ]) →
    Σ ;;; Δ ⊢ σ : Γ →
    Σ ;;; Δ ,, vass na A.[σ] ⊢ ⇑ σ : Γ ,, vass na A.

Lemma well_subst_Up' :
  ∀ Σ Γ Δ σ na t A,
    Σ ;;; Δ ⊢ σ : Γ →
    Σ ;;; Δ ,, vdef na t.[σ] A.[σ] ⊢ ⇑ σ : Γ ,, vdef na t A.



Lemma shift_subst_instance_constr :
  ∀ u t k,
    (subst_instance_constr u t).[⇑^k ↑] = subst_instance_constr u t.[⇑^k ↑].

Lemma inst_subst_instance_constr :
  ∀ u t σ,
    (subst_instance_constr u t).[(subst_instance_constr u ∘ σ)%prog] =
    subst_instance_constr u t.[σ].
Lemma build_branches_type_inst :
  ∀ ind mdecl idecl args u p brs σ,
    closed_ctx (subst_instance_context u (ind_params mdecl)) →
    map_option_out (build_branches_type ind mdecl idecl args u p) = Some brs →
    map_option_out (
        build_branches_type
          ind
          mdecl
          (map_one_inductive_body
             (context_assumptions (ind_params mdecl))
             #|arities_context (ind_bodies mdecl)|
             (fun i : nat ⇒ inst (⇑^i σ))
             (inductive_ind ind)
             idecl
          )
          (map (inst σ) args)
          u
          p.[σ]
    ) = Some (map (on_snd (inst σ)) brs).

Lemma types_of_case_inst :
  ∀ Σ ind mdecl idecl npar args u p pty indctx pctx ps btys σ,
    wf Σ →
    declared_inductive Σ mdecl ind idecl →
    types_of_case ind mdecl idecl (firstn npar args) u p pty =
    Some (indctx, pctx, ps, btys) →
    types_of_case ind mdecl idecl (firstn npar (map (inst σ) args)) u p.[σ] pty.[σ] =
    Some (inst_context σ indctx, inst_context σ pctx, ps, map (on_snd (inst σ)) btys).

Lemma type_inst :
  ∀ Σ Γ Δ σ t A,
    wf Σ.1 →
    wf_local Σ Γ →
    wf_local Σ Δ →
    Σ ;;; Δ ⊢ σ : Γ →
    Σ ;;; Γ |- t : A →
    Σ ;;; Δ |- t.[σ] : A.[σ].

End Sigma.