From Stdlib Require Import List PeanoNat Bool Lia.
From MetaRocq.Utils Require Import utils monad_utils.
From MetaRocq.Common Require Export
     uGraph
     BasicAst
     config. From MetaRocq.Template Require Export
     Ast
     AstUtils
     Induction
     LiftSubst
     UnivSubst
     Typing
     TemplateEnvMap
     TemplateProgram.

Open Scope nat.
Open Scope bs.

Import Template.Ast.
Import ListNotations.

Section Eta.
   Context (Σ : GlobalEnvMap.t).

  Definition eta_single (t : Ast.term) (args : list Ast.term) (ty : Ast.term) (count : nat): term :=
    let needed := count - #|args| in
    let prev_args := map (lift0 needed) args in
    let eta_args := rev_map tRel (seq 0 needed) in
    let remaining := firstn needed (skipn #|args| (rev (smash_context [] (decompose_prod_assum [] ty).1))) in
    let remaining_subst := rev (subst_context (rev args) 0 (rev remaining)) in
    fold_right (fun d b ⇒ Ast.tLambda d.(decl_name) d.(decl_type) b) (mkApps (lift0 needed t) (prev_args ++ eta_args)) remaining_subst.

  Definition eta_constructor (ind : inductive) c u args :=
      match GlobalEnvMap.lookup_constructor Σ ind c with
      | Some (mdecl, idecl, cdecl) ⇒
        let ty := (type_of_constructor mdecl cdecl (ind, c) u) in
        let n := (ind_npars mdecl + context_assumptions (cstr_args cdecl)) in
        Some (eta_single (Ast.tConstruct ind c u) args ty n)
      | _ ⇒ None
      end.

  Definition eta_fixpoint (def : mfixpoint term) (i : nat) d (args : list term) :=
    eta_single (tFix def i) args (d.(dtype)) (1 + d.(rarg)).

  Definition lift_ctx n k (Γ : list (option (nat × term))) :=
    rev (mapi (fun i x ⇒ option_map (on_snd (lift n (k + i))) x) (rev Γ)).

  Definition up (Γ : list (option (nat × term))) := None :: Γ.

  Fixpoint eta_expand (Γ : list (option (nat × term))) (t : term) : term :=
    match t with
    | tVar _ | tSort _ | tProd _ _ _ | tConst _ _ | tInd _ _ ⇒ t
    | tRel n ⇒ match nth_error Γ n with
                | Some (Some (c, ty)) ⇒ eta_single (tRel n) [] (lift0 (S n) ty) c
                | _ ⇒ tRel n
                end

    | tApp hd args ⇒
      match hd with
      | tConstruct ind c u ⇒
        match eta_constructor ind c u (map (eta_expand Γ) args) with
        | Some res ⇒ res
        | None ⇒ tVar ("Error: lookup of an inductive failed for "
                       ++ string_of_kername ind.(inductive_mind))
        end
      | tFix def i ⇒
        let def' :=
          map (fun d ⇒
            let ctx := List.rev (mapi (fun (i : nat) d ⇒ Some (1 + d.(rarg), (lift0 i (dtype d)))) def) in
            {| dname := dname d ; dtype := dtype d ; dbody := eta_expand (ctx ++ Γ) d.(dbody) ; rarg := rarg d |})
            def
        in
        match nth_error def' i with
        | Some d ⇒ eta_fixpoint def' i d (map (eta_expand Γ) args)
        | None ⇒ tVar ("Error: lookup of a fixpoint failed")
        end
      | tRel n ⇒
        match nth_error Γ n with
        | Some (Some (c, ty)) ⇒ eta_single (tRel n) (map (eta_expand Γ) args) (lift0 (S n) ty) c
        | Some None ⇒ mkApps (tRel n) (map (eta_expand Γ) args)
        | _ ⇒ tRel n
        end
      | _ ⇒ mkApps (eta_expand Γ hd) (map (eta_expand Γ) args)
    end
    | tEvar n ts ⇒ tEvar n (map (eta_expand Γ) ts)
    | tLambda na ty body ⇒ tLambda na ty (eta_expand (up Γ) body)
    | tLetIn na val ty body ⇒ tLetIn na (eta_expand Γ val) ty (eta_expand (up Γ) body)
    | tCase ci p disc brs ⇒
        let p' := map_predicate id (eta_expand Γ) id p in
        let brs' := map (fun b ⇒ {| bcontext := bcontext b; bbody := eta_expand (repeat None #|b.(bcontext)| ++ Γ) b.(bbody) |}) brs in
        tCase ci p' (eta_expand Γ disc) brs'
    | tProj p t ⇒ tProj p (eta_expand Γ t)
    | tFix def i ⇒ let def' := (map (fun d ⇒
                                         let ctx := List.rev (mapi (fun (i : nat) d ⇒ Some (1 + d.(rarg), (lift0 i (dtype d)))) def) in
                                        {| dname := dname d ; dtype := dtype d ; dbody := eta_expand (ctx ++ Γ) d.(dbody) ; rarg := rarg d |}) def) in
                      match nth_error def' i with
                      | Some d ⇒ eta_fixpoint def' i d []
                      | None ⇒ tVar ("Error: lookup of a fixpoint failed ")
                      end
    | tCoFix def i ⇒ tCoFix (map (map_def id (eta_expand (repeat None (#|def|) ++ Γ))) def) i
    
    | tConstruct ind c u ⇒
        match eta_constructor ind c u [] with
        | Some res ⇒ res
        | None ⇒ tVar ("Error: lookup of an inductive failed for "
                       ++ string_of_kername ind.(inductive_mind))
        end
    | tCast t1 k t2 ⇒ tCast (eta_expand Γ t1) k (eta_expand Γ t2)
    | tArray u arr def ty ⇒ tArray u (List.map (eta_expand Γ) arr) (eta_expand Γ def) (eta_expand Γ ty)
    | tInt _ | tFloat _ | tString _ ⇒ t
    end.

End Eta.

Definition eta_global_decl Σ cb :=
  {| cst_type := eta_expand Σ [] cb.(cst_type) ;
     cst_universes := cb.(cst_universes) ;
     cst_body := match cb.(cst_body) with
                | Some b ⇒ Some (eta_expand Σ [] b)
                | None ⇒ None
                end;
    cst_relevance := cb.(cst_relevance) |}.

Definition map_decl_body {term : Type} (f : term → term) decl :=
  {| decl_name := decl.(decl_name);
     decl_type := decl.(decl_type);
     decl_body := option_map f decl.(decl_body) |}.

Fixpoint fold_context_k_defs {term : Type} (f : nat → term → term) (Γ: list (BasicAst.context_decl term)) :=
  match Γ with
  | [] ⇒ []
  | d :: Γ ⇒ map_decl_body (f #|Γ|) d :: fold_context_k_defs f Γ
  end.

Lemma context_assumptions_fold_context_k_defs {f : _ → term → term} {Γ} :
  context_assumptions (fold_context_k_defs f Γ) = context_assumptions Γ.
Proof.
  induction Γ; cbn; auto. destruct a as [? [b|] ty]; cbn; auto.
Qed.

Lemma fold_context_k_defs_length {f : _ → term → term} Γ : #|fold_context_k_defs f Γ| = #|Γ|.
Proof.
  induction Γ; cbn; auto.
Qed.

Definition eta_context Σ Γ ctx :=
   
  fold_context_k_defs (fun n ⇒ eta_expand Σ (repeat None (n + Γ))) ctx.

Definition eta_constructor_decl Σ mdecl cdecl :=
  {| cstr_name := cdecl.(cstr_name);
     cstr_args := eta_context Σ (#|mdecl.(ind_params)| + #|mdecl.(ind_bodies)|) cdecl.(cstr_args);
     cstr_indices := map (eta_expand Σ []) cdecl.(cstr_indices);
     cstr_type := eta_expand Σ (repeat None #|mdecl.(ind_bodies)|) cdecl.(cstr_type);
     cstr_arity := cdecl.(cstr_arity) |}.

Definition eta_inductive_decl Σ mdecl idecl :=
  {| ind_name := idecl.(ind_name);
           ind_indices := idecl.(ind_indices);
     ind_sort := idecl.(ind_sort);
     ind_type := idecl.(ind_type);
     ind_kelim := idecl.(ind_kelim);
     ind_ctors := map (eta_constructor_decl Σ mdecl) idecl.(ind_ctors);
     ind_projs := idecl.(ind_projs);
     ind_relevance := idecl.(ind_relevance) |}.

Definition eta_minductive_decl Σ mdecl :=
  {| ind_finite := mdecl.(ind_finite);
     ind_params := eta_context Σ 0 mdecl.(ind_params);
     ind_npars := mdecl.(ind_npars);
     ind_bodies := map (eta_inductive_decl Σ mdecl) mdecl.(ind_bodies);
     ind_universes := mdecl.(ind_universes);
     ind_variance := mdecl.(ind_variance); |}.

Definition eta_global_declaration (Σ : GlobalEnvMap.t) decl : global_decl :=
  match decl with
  | ConstantDecl cb ⇒ ConstantDecl (eta_global_decl Σ cb)
  | InductiveDecl idecl ⇒ InductiveDecl (eta_minductive_decl Σ idecl)
  end.

Definition eta_global_declarations (Σ : GlobalEnvMap.t) (decls : global_declarations) :=
  map (on_snd (eta_global_declaration Σ)) decls.

Definition eta_expand_global_env (Σ : GlobalEnvMap.t) : global_env :=
  {| universes := Σ.(universes); declarations := eta_global_declarations Σ Σ.(declarations);
     retroknowledge := Σ.(retroknowledge) |}.

Definition eta_expand_program (p : template_program_env) : Ast.Env.program :=
  let Σ' := eta_expand_global_env p.1 in
  (Σ', eta_expand p.1 [] p.2).


Definition isConstruct t :=
    match t with tConstruct _ _ _ ⇒ true | _ ⇒ false end.
Definition isFix t :=
    match t with tFix _ _ ⇒ true | _ ⇒ false end.
Definition isRel t :=
    match t with tRel _ ⇒ true | _ ⇒ false end.

Section expanded.

Variable Σ : global_env.

Local Unset Elimination Schemes.

Inductive expanded (Γ : list nat): term → Prop :=
| expanded_tRel (n : nat) : nth_error Γ n = Some 0 → expanded Γ (tRel n)
| expanded_tRel_app (n : nat) args m : nth_error Γ n = Some m → m ≤ #|args| → Forall (expanded Γ) args → expanded Γ (tApp (tRel n) args)
| expanded_tVar (id : ident) : expanded Γ (tVar id)
| expanded_tEvar (ev : nat) (args : list term) : Forall (expanded Γ) args → expanded Γ (tEvar ev args)
| expanded_tSort (s : sort) : expanded Γ (tSort s)
| expanded_tCast (t : term) (kind : cast_kind) (v : term) : expanded Γ t → expanded Γ v → expanded Γ (tCast t kind v)
| expanded_tProd (na : aname) (ty : term) (body : term) : expanded Γ (tProd na ty body)
| expanded_tLambda (na : aname) (ty : term) (body : term) : expanded (0 :: Γ) body → expanded Γ (tLambda na ty body)
| expanded_tLetIn (na : aname) (def : term) (def_ty : term) (body : term) : expanded Γ def → expanded (0 :: Γ) body → expanded Γ (tLetIn na def def_ty body)
| expanded_tApp (f : term) (args : list term) : negb (isConstruct f || isFix f || isRel f) → expanded Γ f → Forall (expanded Γ) args → expanded Γ (tApp f args)
| expanded_tConst (c : kername) (u : Instance.t) : expanded Γ (tConst c u)
| expanded_tInd (ind : inductive) (u : Instance.t) : expanded Γ (tInd ind u)
| expanded_tConstruct (ind : inductive) (idx : nat) (u : Instance.t) mind idecl cdecl :
    declared_constructor Σ (ind, idx) mind idecl cdecl →
    ind_npars mind + context_assumptions (cstr_args cdecl) = 0 →
    expanded Γ (tConstruct ind idx u)
| expanded_tCase (ci : case_info) (type_info:predicate term)
        (discr:term) (branches : list (branch term)) :
    expanded Γ discr →
    Forall (expanded Γ) type_info.(pparams) →
    Forall (fun br ⇒ expanded (repeat 0 #|br.(bcontext)| ++ Γ) br.(bbody)) branches →
    expanded Γ (tCase ci type_info discr branches)
| expanded_tProj (proj : projection) (t : term) : expanded Γ t → expanded Γ (tProj proj t)
| expanded_tFix (mfix : mfixpoint term) (idx : nat) args d :
  d.(rarg) < context_assumptions (decompose_prod_assum [] d.(dtype)).1 →
  Forall (fun d ⇒ isLambda d.(dbody) ∧
           let ctx := List.rev (mapi (fun (i : nat) d ⇒ 1 + d.(rarg)) mfix) in
          expanded (ctx ++ Γ) d.(dbody)) mfix →
  Forall (expanded Γ) args →
  args ≠ [] →
  nth_error mfix idx = Some d →
  #|args| > d.(rarg) →
  expanded Γ (tApp (tFix mfix idx) args)
| expanded_tCoFix (mfix : mfixpoint term) (idx : nat) :
  Forall (fun d ⇒ expanded (repeat 0 #|mfix| ++ Γ) d.(dbody)) mfix →
  expanded Γ (tCoFix mfix idx)
| expanded_tConstruct_app ind c u mind idecl cdecl args :
    declared_constructor Σ (ind, c) mind idecl cdecl →
    #|args| ≥ (ind_npars mind + context_assumptions (cstr_args cdecl)) →
    Forall (expanded Γ) args →
    expanded Γ (tApp (tConstruct ind c u) args)
| expanded_tInt i : expanded Γ (tInt i)
| expanded_tFloat f : expanded Γ (tFloat f)
| expanded_tString s : expanded Γ (tString s)
| expanded_tArray u arr def ty :
  Forall (expanded Γ) arr →
  expanded Γ def →
  expanded Γ ty →
  expanded Γ (tArray u arr def ty).

End expanded.

Lemma expanded_ind :
∀ (Σ : global_env) (P : list nat → term → Prop),
(∀ Γ, ∀ n : nat, nth_error Γ n = Some 0 → P Γ (tRel n)) →
(∀ Γ, ∀ n : nat, ∀ args, ∀ m, nth_error Γ n = Some m → ∀ Heq : m ≤ #|args|, Forall (expanded Σ Γ) args → Forall (P Γ) args → P Γ (tApp (tRel n) args)) →
(∀ Γ, ∀ id : ident, P Γ (tVar id)) →
(∀ Γ, ∀ (ev : nat) (args : list term), Forall (expanded Σ Γ) args → Forall (P Γ) args → P Γ (tEvar ev args)) →
(∀ Γ, ∀ s : sort, P Γ (tSort s)) →
(∀ Γ, ∀ (t : term) (kind : cast_kind) (v : term),
 expanded Σ Γ t → P Γ t → expanded Σ Γ v → P Γ v → P Γ (tCast t kind v)) →
(∀ Γ, ∀ (na : aname) (ty body : term), P Γ (tProd na ty body)) →
(∀ Γ, ∀ (na : aname) (ty body : term), expanded Σ (0 :: Γ) body → P (0 :: Γ) body → P Γ (tLambda na ty body)) →
(∀ Γ (na : aname) (def def_ty body : term),
 expanded Σ Γ def →
 P Γ def →
 expanded Σ (0 :: Γ) body → P (0 :: Γ) body → P Γ (tLetIn na def def_ty body)) →
(∀ Γ, ∀ (f7 : term) (args : list term),
 negb (isConstruct f7 || isFix f7 || isRel f7) → ¬ isRel f7 →
 expanded Σ Γ f7 → P Γ f7 → Forall (expanded Σ Γ) args → Forall (P Γ) args → P Γ (tApp f7 args)) →
(∀ Γ (c : kername) (u : Instance.t), P Γ (tConst c u)) →
(∀ Γ, ∀ (ind : inductive) (u : Instance.t), P Γ (tInd ind u)) →
(∀ Γ, ∀ (ind : inductive) (idx : nat) (u : Instance.t)
   (mind : mutual_inductive_body) (idecl : one_inductive_body)
   (cdecl : constructor_body),
 declared_constructor Σ (ind, idx) mind idecl cdecl →
 ind_npars mind + context_assumptions (cstr_args cdecl) = 0 →
 P Γ (tConstruct ind idx u)) →
(∀ Γ (ci : case_info) (type_info : predicate term)
   (discr : term) (branches : list (branch term)),
 expanded Σ Γ discr →
 P Γ discr →
 Forall (expanded Σ Γ) type_info.(pparams) →
 Forall (P Γ) type_info.(pparams) →
 Forall (fun br : branch term ⇒ expanded Σ (repeat 0 #|br.(bcontext)| ++ Γ) (bbody br)) branches →
 Forall (fun br : branch term ⇒ P (repeat 0 #|br.(bcontext)| ++ Γ)%list (bbody br)) branches →
 P Γ (tCase ci type_info discr branches)) →
(∀ Γ (proj : projection) (t : term),
 expanded Σ Γ t → P Γ t → P Γ (tProj proj t)) →
(∀ Γ (mfix : mfixpoint term) (idx : nat) d args,
  d.(rarg) < context_assumptions (decompose_prod_assum [] d.(dtype)).1 →
  Forall (fun d ⇒ isLambda d.(dbody) ∧ let ctx := List.rev (mapi (fun (i : nat) d ⇒ 1 + d.(rarg)) mfix) in expanded Σ (ctx ++ Γ) d.(dbody)) mfix →
  Forall (fun d ⇒ let ctx := List.rev (mapi (fun (i : nat) d ⇒ 1 + d.(rarg)) mfix) in P (ctx ++ Γ)%list d.(dbody)) mfix →
  Forall (expanded Σ Γ) args →
  Forall (P Γ) args →
  args ≠ [] →
  nth_error mfix idx = Some d →
  #|args| > d.(rarg) →
  P Γ (tApp (tFix mfix idx) args)) →
(∀ Γ (mfix : mfixpoint term) (idx : nat),
  Forall (fun d ⇒ expanded Σ (repeat 0 #|mfix| ++ Γ) d.(dbody)) mfix →
  Forall (fun d ⇒ P (repeat 0 #|mfix| ++ Γ)%list d.(dbody)) mfix →
  P Γ (tCoFix mfix idx)) →
(∀ Γ (ind : inductive) (c : nat) (u : Instance.t)
   (mind : mutual_inductive_body) (idecl : one_inductive_body)
   (cdecl : constructor_body) (args : list term),
 declared_constructor Σ (ind, c) mind idecl cdecl →
 #|args| ≥ ind_npars mind + context_assumptions (cstr_args cdecl) →
 Forall (expanded Σ Γ) args →
 Forall (P Γ) args →
 P Γ(tApp (tConstruct ind c u) args)) →
(∀ Γ i, P Γ (tInt i)) →
(∀ Γ f, P Γ (tFloat f)) →
(∀ Γ s, P Γ (tString s)) →
(∀ Γ u arr def ty,
  Forall (P Γ) arr →
  P Γ def →
  P Γ ty →
  P Γ (tArray u arr def ty)) →
 ∀ Γ, ∀ t : term, expanded Σ Γ t → P Γ t.
Proof.
  intros Σ P HRel HRel_app HVar HEvar HSort HCast HProd HLamdba HLetIn HApp HConst HInd HConstruct HCase HProj HFix HCoFix HConstruct_app Hint Hfloat Hstring Harr.
  fix f 3.
  intros Γ t Hexp. destruct Hexp; eauto.
  all: match goal with [H : Forall _ _ |- _] ⇒ let all := fresh "all" in rename H into all end.
  - eapply HRel_app; eauto. clear - f all. induction all; econstructor; eauto.
  - eapply HEvar; eauto. clear - f all. induction all; econstructor; eauto.
  - eapply HApp; eauto. destruct f0; cbn in *; eauto.
    clear - f all; induction all; econstructor; eauto.
  - eapply HCase; eauto.
    induction H; econstructor; eauto.
    induction all; econstructor; eauto.
  - assert (Forall (P Γ) args). { clear - f all. induction all; econstructor; eauto. }
    eapply HFix; eauto.
    revert H0. clear - f.
    generalize mfix at 1 3. intros mfix0 H. induction H; econstructor; cbn in *; intuition eauto; split.
  - eapply HCoFix; eauto.
    revert all. clear - f.
    generalize mfix at 1 3. intros mfix0 H. induction H; econstructor; cbn in *; eauto; split.
  - eapply HConstruct_app; eauto.
    clear - all f. induction all; econstructor; eauto.
  - eapply Harr; eauto. clear -all f. induction all; constructor; auto.
Qed.

Local Hint Constructors expanded : core.

Record expanded_constant_decl Σ (cb : Ast.Env.constant_body) : Prop :=
  { expanded_body : on_Some_or_None (expanded Σ []) cb.(Ast.Env.cst_body); }.

Definition expanded_context Σ Γ ctx :=
  ∥ All_fold (fun Δ d ⇒ ForOption (expanded Σ (repeat 0 #|Δ| ++ Γ)) d.(decl_body)) ctx ∥.

Record expanded_constructor_decl Σ mdecl cdecl :=
  { expanded_cstr_args : expanded_context Σ (repeat 0 (#|mdecl.(ind_params)| + #|mdecl.(ind_bodies)|)) cdecl.(cstr_args);
    
    expanded_cstr_type : expanded Σ (repeat 0 #|mdecl.(ind_bodies)|) cdecl.(cstr_type) }.

Record expanded_inductive_decl Σ mdecl idecl :=
  {
    expanded_ind_ctors : Forall (expanded_constructor_decl Σ mdecl) idecl.(ind_ctors) }.

Record expanded_minductive_decl Σ mdecl :=
  { expanded_params : expanded_context Σ [] mdecl.(ind_params);
    expanded_ind_bodies : Forall (expanded_inductive_decl Σ mdecl) mdecl.(ind_bodies) }.

Definition expanded_decl Σ d :=
  match d with
  | Ast.Env.ConstantDecl cb ⇒ expanded_constant_decl Σ cb
  | Ast.Env.InductiveDecl idecl ⇒ expanded_minductive_decl Σ idecl
  end.

Inductive expanded_global_declarations (univs : ContextSet.t) (retro : Environment.Retroknowledge.t) : ∀ (Σ : Ast.Env.global_declarations), Prop :=
| expanded_global_nil : expanded_global_declarations univs retro []
| expanded_global_cons decl Σ : expanded_global_declarations univs retro Σ →
  expanded_decl {| Ast.Env.universes := univs; Ast.Env.declarations := Σ; Ast.Env.retroknowledge := retro |} decl.2 →
  expanded_global_declarations univs retro (decl :: Σ).

Definition expanded_global_env (g : Ast.Env.global_env) :=
  expanded_global_declarations g.(Ast.Env.universes) g.(Ast.Env.retroknowledge) g.(Ast.Env.declarations).

Definition expanded_program (p : Ast.Env.program) :=
  expanded_global_env p.1 ∧ expanded p.1 [] p.2.

Definition isFix_app t :=
  match fst (decompose_app t) with
  | tFix _ _ ⇒ true
  | _ ⇒ false
  end.

Definition isRel_app t :=
  match fst (decompose_app t) with
  | tRel _ ⇒ true
  | _ ⇒ false
  end.

Lemma expanded_fold_lambda Σ Γ t l :
  expanded Σ Γ
    (fold_right (fun d (b : term) ⇒ tLambda d.(decl_name) d.(decl_type) b) t l) ↔ expanded Σ (repeat 0 #|l| ++ Γ) t.
Proof.
  induction l as [ | []] in t, Γ |- *; cbn - [repeat] in ×.
  - reflexivity.
  - replace (S #|l|) with (#|l| + 1) by lia.
    rewrite repeat_app. cbn. rewrite <- app_assoc. cbn.
    split.
    + inversion 1; subst. now eapply IHl.
    + intros. econstructor. now eapply IHl.
Qed.

Lemma expanded_mkApps_tConstruct Σ Γ mind idecl cdecl ind idx u args :
  declared_constructor Σ (ind, idx) mind idecl cdecl →
  #|args| ≥ ind_npars mind + context_assumptions (cstr_args cdecl) →
  Forall (expanded Σ Γ) args →
  expanded Σ Γ (mkApps (tConstruct ind idx u) args).
Proof.
  intros Hdecl Heq. unfold mkApps.
  destruct args eqn:E.
  - econstructor; eauto. cbn in ×. lia.
  - eapply expanded_tConstruct_app; eauto.
Qed.

Lemma expanded_mkApps_tFix Σ Γ mfix idx d args :
  d.(rarg) < context_assumptions (decompose_prod_assum [] d.(dtype)).1 →
  nth_error mfix idx = Some d →
  #|args| ≥ S (d.(rarg)) →
  Forall (fun d0 : def term ⇒ isLambda d0.(dbody) ∧
    let ctx := List.rev (mapi (fun (_ : nat) (d1 : def term) ⇒ 1 + rarg d1) mfix) in expanded Σ (ctx ++ Γ) (dbody d0)) mfix →
  Forall (expanded Σ Γ) args →
  args ≠ [] →
  expanded Σ Γ (mkApps (tFix mfix idx) args).
Proof.
  intros Hdecl Heq. unfold mkApps.
  destruct args eqn:E.
  - congruence.
  - intros. eapply expanded_tFix; eauto.
Qed.

Lemma expanded_mkApps_tFix_inv Σ Γ mfix idx args :
  expanded Σ Γ (mkApps (tFix mfix idx) args) →
  Forall (fun d0 : def term ⇒ isLambda d0.(dbody) ∧ let ctx := List.rev (mapi (fun (_ : nat) (d1 : def term) ⇒ 1 + rarg d1) mfix) in expanded Σ (ctx ++ Γ) (dbody d0)) mfix.
Proof.
  induction args.
  - cbn. inversion 1.
  - cbn. inversion 1; subst; cbn in *; try congruence.
Qed.

Lemma expanded_tApp_args Σ Γ t args :
  expanded Σ Γ (tApp t args) →
  Forall (expanded Σ Γ) args.
Proof.
  inversion 1; subst; eauto.
Qed.

Lemma expanded_tApps_inv Σ Γ t args :
  expanded Σ Γ (tApp t args) →
  ∀ args', #|args'| ≥ #|args| →
  Forall (expanded Σ Γ) args' →
  expanded Σ Γ (tApp t args').
Proof.
  intros. invs H.
  - econstructor; eauto. lia.
  - eauto.
  - eapply expanded_tFix; eauto.
    destruct args, args'; cbn in *; lia || congruence.
    lia.
  - eapply expanded_tConstruct_app; eauto.
    lia.
Qed.

Lemma expanded_mkApps_inv Σ Γ t args :
  expanded Σ Γ (mkApps t args) →
  ∀ args', #|args'| ≥ #|args| →
  Forall (expanded Σ Γ) args' →
  expanded Σ Γ (mkApps t args').
Proof.
  intros.
  destruct args' in t, args, H, H0, H1 |- ×.
  - destruct args; cbn in *; try lia. eauto.
  - destruct args; cbn in ×.
    + destruct t; try now (eapply expanded_tApps_inv; eauto).
      × invs H. econstructor; eauto.
      × eapply expanded_tApps_inv. eauto. len; lia.
        eapply app_Forall; eauto. eapply expanded_tApp_args; eauto.
      × invs H. eapply expanded_tConstruct_app; eauto. cbn; lia.
    + destruct t; try now (eapply expanded_tApps_inv; eauto).
      eapply expanded_tApps_inv. eauto. len; lia.
      eapply app_Forall; eauto. eapply expanded_tApp_args in H.
      eapply Forall_app in H. eapply H.
Qed.

Lemma expanded_mkApps Σ Γ f args :
  expanded Σ Γ f → Forall (expanded Σ Γ) args →
  expanded Σ Γ (mkApps f args).
Proof.
  intros.
  eapply expanded_mkApps_inv with (args := []); cbn; eauto. lia.
Qed.

Local Hint Rewrite repeat_length length_combine : len.
Local Hint Rewrite <- app_assoc : list.

Lemma apply_expanded Σ Γ Γ' t t' :
  expanded Σ Γ t → Γ = Γ' → t = t' → expanded Σ Γ' t'.
Proof. intros; now subst. Qed.

Lemma ext_lift n m n' m' t :
  n' = n → m' = m → lift n m t = lift n' m' t.
Proof. intros; now subst. Qed.

Lemma decompose_prod_lift t n m :
  #|(decompose_prod t).1.1| = #|(decompose_prod (lift n m t)).1.1|.
Proof.
  induction t in n, m |- *; cbn; try lia.
  destruct (decompose_prod t2) as [[]]; cbn in ×.
  specialize (IHt2 n (S m)).
  destruct (decompose_prod (lift n (S m) t2)) as [[]]; cbn in ×. lia.
Qed.

Lemma context_assumptions_lift' t Γ Γ' n m :
context_assumptions Γ = context_assumptions Γ' →
context_assumptions (decompose_prod_assum Γ t).1 =
context_assumptions (decompose_prod_assum Γ' (lift n m t)).1.
Proof.
  intros Hlen.
  induction t in Γ, Γ', Hlen, n, m |- *; cbn; try lia.
  - eapply IHt2. cbn; lia.
  - eapply IHt3. cbn; lia.
Qed.

Lemma context_assumptions_lift t n m :
context_assumptions (decompose_prod_assum [] t).1 =
context_assumptions (decompose_prod_assum [] (lift n m t)).1.
Proof.
  now eapply context_assumptions_lift'.
Qed.

Lemma isLambda_unlift n k t : isLambda (lift n k t) → isLambda t.
Proof.
  destruct t; auto.
Qed.

Lemma expanded_unlift {Σ : global_env} Γ' Γ'' Γ t Γgoal :
  expanded Σ (Γ' ++ Γ'' ++ Γ) (lift #|Γ''| #|Γ'| t) →
  (Γ' ++ Γ)%list = Γgoal →
  expanded Σ Γgoal t.
Proof.
  intros Hexp <-.
  remember (Γ' ++ Γ'' ++ Γ)%list as Γ_.
  remember ((lift #|Γ''| #|Γ'| t)) as t_.
  induction Hexp in Γ', Γ'', Γ, HeqΓ_, Heqt_, t |- *; cbn; subst; destruct t; invs Heqt_; eauto.
  - rename n0 into n. econstructor. destruct (Nat.leb_spec #|Γ'| n).
    + rewrite !nth_error_app2 in H |- *; try lia.
      rewrite !nth_error_app2 in H; try lia. rewrite <- H. f_equal. lia.
    + rewrite nth_error_app1 in H |- *; try lia. eauto.
  - destruct t; invs H3. econstructor. 3:{ eapply Forall_map_inv in H0, H1. solve_all. }
    revert H. len. intros H. destruct (Nat.leb_spec #|Γ'| n0).
    + rewrite !nth_error_app2 in H |- *; try lia.
      rewrite !nth_error_app2 in H; try lia. rewrite <- H. f_equal. lia.
    + rewrite nth_error_app1 in H |- *; try lia. eauto.
    + revert Heq. len. lia.
  - econstructor. solve_all.
  - econstructor. rewrite app_comm_cons. eapply IHHexp; try reflexivity.
  - econstructor; eauto. rewrite app_comm_cons. eapply IHHexp2. 2: now simpl_list. eauto.
  - econstructor; eauto. destruct t; cbn in *; eauto.
    solve_all.
  - econstructor; eauto. solve_all. cbn in H0.
    eapply All_map_inv in H0; solve_all. solve_all.
    specialize (b (repeat 0 #|bcontext x| ++ Γ')%list Γ'' Γ).
    autorewrite with list len in b. now eapply b.
  - destruct t; invs H8.
    rewrite !nth_error_map in H5. destruct (nth_error mfix0 idx0) eqn:EE; cbn in H5; invs H5.
    eapply expanded_tFix.
    + shelve.
    + eapply Forall_map_inv in H0, H1, H3. cbn in ×.
      solve_all. now apply isLambda_unlift in H0. rewrite app_assoc.
      eapply b. autorewrite with list. f_equal. f_equal.
      rewrite mapi_map. eapply mapi_ext. intros. cbn. reflexivity.
      f_equal. now len.
    + solve_all.
    + destruct args0; cbn in *; congruence.
    + eauto.
    + revert H6. len. lia.
     Unshelve. revert H6. len. cbn in ×. rewrite <- context_assumptions_lift in H. lia.
  - econstructor. solve_all. rewrite app_assoc.
    eapply b. autorewrite with len list. reflexivity. now len.
  - destruct t; invs H4.
    eapply expanded_tConstruct_app; eauto. revert H0.
    now len. solve_all.
  - constructor; eauto. solve_all.
Qed.

Lemma expanded_lift {Σ : global_env} Γ' Γ'' Γ t :
  expanded Σ (Γ' ++ Γ) t →
  expanded Σ (Γ' ++ Γ'' ++ Γ) (lift #|Γ''| #|Γ'| t).
Proof.
  remember (Γ' ++ Γ)%list as Γ_.
  induction 1 in Γ', Γ'', Γ, HeqΓ_ |- *; cbn; eauto; subst.
  - econstructor. destruct (Nat.leb_spec #|Γ'| n).
    + rewrite !nth_error_app2 in H |- *; try lia.
      rewrite !nth_error_app2; try lia. rewrite <- H. f_equal. lia.
    + rewrite nth_error_app1 in H |- *; try lia. eauto.
  - econstructor. 3: solve_all.
    destruct (Nat.leb_spec #|Γ'| n).
    + rewrite !nth_error_app2 in H |- *; try lia.
      rewrite nth_error_app2; try lia. rewrite <- H.
      f_equal. lia.
    + rewrite nth_error_app1 in H |- *; try lia; eauto.
    + len. lia.
  - econstructor; solve_all.
  - econstructor. rewrite app_comm_cons. eapply IHexpanded. now simpl_list.
  - econstructor; eauto. rewrite app_comm_cons. eapply IHexpanded2. now simpl_list.
  - econstructor; eauto. destruct f7; cbn in *; eauto.
    solve_all.
  - econstructor; eauto. solve_all. cbn; solve_all.
    solve_all. specialize (a (repeat 0 #|bcontext x| ++ Γ')%list Γ'' Γ).
    autorewrite with list len in a. now eapply a.
  - eapply expanded_tFix.
    + shelve.
    + solve_all. eapply apply_expanded. eapply a.
      now rewrite app_assoc.
      autorewrite with list. f_equal. f_equal.
      rewrite mapi_map. eapply mapi_ext. intros. cbn. reflexivity.
      f_equal. now len.
    + solve_all.
    + destruct args; cbn in *; congruence.
    + now rewrite !nth_error_map, H5.
    + len. lia.
    Unshelve. cbn.
    rewrite <- !context_assumptions_lift. lia.
  - econstructor. solve_all.
    unshelve epose proof (a (_ ++ _)%list _ _ _). 5: now rewrite <- app_assoc.
    shelve. autorewrite with len list in H |- ×. eapply H.
  - eapply expanded_tConstruct_app; eauto.
    now len. solve_all.
  - constructor; eauto. eapply Forall_map. solve_all.
Qed.

Lemma expanded_lift' {Σ : global_env} Γ' Γ'' Γ t Γassum Γgoal n m :
  (Γ' ++ Γ)%list = Γassum →
  (Γ' ++ Γ'' ++ Γ)%list = Γgoal →
  #|Γ''| = n → #|Γ'| = m →
  expanded Σ Γassum t →
  expanded Σ Γgoal (lift n m t).
Proof.
  intros. subst. now eapply expanded_lift.
Qed.

Lemma Forall_typing_spine_Forall {cf : config.checker_flags} Σ Γ (P : term → Prop) t_ty l t' s :
  Forall_typing_spine Σ Γ
       (fun t _ : term ⇒ P t) t_ty l t' s →
  Forall P l.
Proof.
  induction 1; econstructor; eauto.
Qed.

Lemma nth_map' {A B} (f : A → B) n l d d' :
  (d' = f d) →
  nth n (map f l) d' = f (nth n l d).
Proof.
  induction n in l |- *; destruct l; simpl; auto.
Qed.

Lemma decompose_prod12 t :
  #| (decompose_prod t).1.1| = #|(decompose_prod t).1.2|.
Proof.
  induction t; cbn; try lia.
  do 2 destruct decompose_prod as [[]]. cbn in ×. lia.
Qed.

Lemma mkApps_tRel:
∀ (n : nat) (l : list term), l ≠ nil →
mkApps (tRel n) (l) = tApp (tRel n) (l).
Proof.
  destruct l; cbn; try congruence.
Qed.

Lemma expanded_eta_single_tRel_app Σ0 n l n0 Γ' T :
  expanded Σ0
    (map
      (fun x : option (nat × term) ⇒
        match x with
        | Some p ⇒ let (n1, _) := p in n1
        | None ⇒ 0
        end) Γ') (eta_single (tRel n) [] T n0) →
        Forall (expanded Σ0
        (map
        (fun x : option (nat × term) ⇒
        match x with
        | Some p ⇒ let (n1, _) := p in n1
        | None ⇒ 0
        end) Γ')) l →
        n0 ≤ context_assumptions (decompose_prod_assum [] T).1 →
  expanded Σ0
    (map
      (fun x : option (nat × term) ⇒
        match x with
        | Some p ⇒ let (n1, _) := p in n1
        | None ⇒ 0
        end) Γ') (eta_single (tRel n) l T n0).
Proof.
  intros H Hl Hlen. unfold eta_single in ×.
  rewrite expanded_fold_lambda in H |- ×.
  rewrite Nat.sub_0_r in H. cbn in H.
  destruct n0.
  - cbn in ×. invs H. simpl_list. eapply expanded_mkApps.
    eauto. solve_all.
    now rewrite lift0_id.
  - rewrite mkApps_tRel in H. 2:
    { replace (S n0) with (n0 + 1) by lia. rewrite rev_map_spec.
      rewrite seq_app, map_app, rev_app_distr. cbn. congruence. }
    invs H; cbn - [rev_map seq] in H2; try congruence.
    autorewrite with len list in H2 |- ×.
    rewrite !length_firstn in H2 |- ×.
    rewrite !List.length_skipn.
    autorewrite with len in H2 |- ×.
    replace ((Init.Nat.min (S n0)
    (#|[]| + context_assumptions (decompose_prod_assum [] T).1))) with (S n0) in H2. 2:{
        len. rewrite rev_map_spec in H3. autorewrite with len in H3. cbn in H3.
        rewrite length_seq in H3. destruct context_assumptions; try lia.
    } cbn in H2.
    unfold lift0 at 1.
    rewrite mkApps_tRel. 2:{ destruct l; cbn - [rev_map]; try congruence. rewrite rev_map_spec. cbn. clear. destruct List.rev; cbn; try congruence. }
    econstructor.
    {
      replace ((Init.Nat.min (S n0 - #|l|)
      (#|[]| + context_assumptions (decompose_prod_assum [] T).1 - #|l|))) with (S n0 - #|l|). 2:{ len. destruct #|l|; lia. }
    assert (0 <=? n = true) as → by now destruct n.
    rewrite <- H2.
    rewrite !nth_error_app2. 2,3: rewrite repeat_length; lia.
    f_equal. rewrite !repeat_length. lia.
    }
    revert H3. len. rewrite !length_seq. destruct l; cbn; lia.
    eapply app_Forall.
    + Opaque minus. solve_all. eapply @expanded_lift' with (Γ' := []). cbn; reflexivity.
      cbn; reflexivity. 2: reflexivity. len. lia. eauto.
    + change ((0 :: seq 1 n0)) with (seq 0 (S n0)) in ×.
      assert (S n0 > #|l| ∨ S n0 ≤ #|l|) as [HH | HH] by lia.
      assert (S n0 = S n0 - #|l| + #|l|) as EE by lia.
      2:{ replace (S n0 - #|l|) with 0 by lia. cbn. econstructor. }
      rewrite EE in H4.
      rewrite seq_app, rev_map_spec, map_app, rev_app_distr in H4.
      eapply Forall_app in H4 as []. rewrite Nat.min_l. 2: len; lia.
      rewrite <- EE in H0.
    revert H0. len. rewrite !length_firstn, Nat.min_l. 2:len;lia.
    rewrite rev_map_spec. intros.
    rewrite Forall_forall in H0 |- ×. intros.
    specialize (H0 _ H1). rewrite <- in_rev in H1.
    eapply in_map_iff in H1 as (? & <- & [_ ?] % in_seq).
    invs H0.
    econstructor. rewrite nth_error_app1. 2: rewrite repeat_length; lia.
    eapply nth_error_repeat. lia.
Qed.

 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').
Proof.
  intros n k c k'.
  pose proof (to_extended_list_k_spec c k').
  symmetry. solve_all.
  destruct H as [x' [-> Hx']]. intuition. simpl.
  destruct (leb_spec_Set k x').
  - lia.
  - reflexivity.
Qed.

 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 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 u) args)).
Proof.
 intros.
 rewrite subst_instance_mkApps, subst_mkApps.
 f_equal.
 - subst head. unfold subst_instance. cbn[subst_instance_constr].
   rewrite (subst_rel_eq _ _ (#|ind_bodies mdecl| - S (inductive_ind ind)) (tInd ind u)); cbn; try lia; auto.
   subst s. rewrite inds_spec, rev_mapi, nth_error_mapi.
   elim nth_error_spec.
   + intros. simpl.
     f_equal. destruct ind; simpl. f_equal. f_equal. simpl in H. lia.
   + rewrite List.length_rev. lia.
 - rewrite !map_app. f_equal.
   rewrite map_subst_instance_to_extended_list_k.
   erewrite to_extended_list_k_map_subst at 2.
   + now rewrite Nat.add_comm.
   + lia.
Qed.

Lemma decompose_type_of_constructor :
  ∀ cf: config.checker_flags
, ∀ Σ0: global_env_ext
, ∀ wfΣ: wf Σ0.1
, ∀ ind: inductive
, ∀ i: nat
, ∀ u: Instance.t
, ∀ mdecl: mutual_inductive_body
, ∀ idecl: one_inductive_body
, ∀ cdecl: constructor_body
, ∀ isdecl': declared_constructor Σ0.1 (ind, i) mdecl idecl cdecl,
context_assumptions
     (decompose_prod_assum [] (type_of_constructor mdecl cdecl (ind, i) u)).1 = ind_npars mdecl + context_assumptions (cstr_args cdecl).
Proof.
  intros. red in wfΣ.
  unfold type_of_constructor.
  destruct isdecl' as [[Hmdecl Hidecl] Hcdecl]. red in Hmdecl.
  eapply lookup_global_Some_iff_In_NoDup in Hmdecl; eauto.
  2: destruct wfΣ; now eapply NoDup_on_global_decls.
  eapply lookup_on_global_env in Hmdecl; eauto.
  destruct Hmdecl as (Σ' & wfΣ' & Hext & [Hind Hparam Hnpars Hvar]).
  unfold type_of_constructor.
  eapply nth_error_alli in Hind; eauto.
  destruct Hind.
  red in onConstructors.
  eapply All2_nth_error_Some in onConstructors; eauto.
  destruct onConstructors as (univs & Hnth & H).
  destruct H.
  rewrite cstr_eq. cbn.
  rewrite !subst_instance_it_mkProd_or_LetIn.
  rewrite !subst_it_mkProd_or_LetIn.
  rewrite <- it_mkProd_or_LetIn_app.
  rewrite !decompose_prod_assum_it_mkProd.
  - cbn. rewrite app_nil_r, !context_assumptions_app. now len.
  - unfold cstr_concl, cstr_concl_head. rewrite Nat.add_0_r. len.
    rewrite subst_cstr_concl_head.
    eapply is_ind_app_head_mkApps.
    eapply nth_error_Some_length; eauto.
Qed.

Lemma wf_fixpoint_rarg :
  ∀ cf: config.checker_flags
, ∀ Σ0: global_env_ext
, ∀ wfΣ: wf Σ0.1
, ∀ mfix: list (def term)
, ∀ decl: def term
, ∀ H2: wf_fixpoint Σ0.1 mfix, In decl mfix →
decl.(rarg) < context_assumptions (decompose_prod_assum [] decl.(dtype)).1.
Proof.
  intros.
  unfold wf_fixpoint in H2.
  eapply andb_and in H2. destruct H2 as [_ H2].
  destruct map_option_out eqn:E; try congruence.
  destruct l eqn:E2; try congruence.
  rewrite <- E2 in ×. clear E2 H2 k l0.
  induction mfix in l, E, H |- ×.
  - inversion H.
  - cbn in E. destruct (check_one_fix a) eqn:Ea; try congruence.
    destruct H as [-> | H].
    + unfold check_one_fix in Ea. destruct decl; cbn.
      destruct (decompose_prod_assum) eqn:Eprod; try congruence. unfold destInd in Ea.
      destruct nth_error eqn:Enth; try congruence.
      eapply nth_error_Some_length in Enth.
      revert Enth. now len.
    + destruct map_option_out eqn:?; try congruence. eapply IHmfix; eauto.
Qed.

From Equations Require Import Equations.

Lemma typing_wf_fixpoint {cf : config.checker_flags} Σ0 Γ0 mfix idx t_ty :
   Σ0;;; Γ0 |- tFix mfix idx : t_ty → wf_fixpoint Σ0 mfix.
Proof.
  intros H.
  depind H; eauto.
Qed.

Lemma isLambda_eta_expand Σ Γ t :
  isLambda t → isLambda (eta_expand Σ Γ t).
Proof. destruct t; auto. Qed.


Import EnvMap.

Definition repr_decls Σg Σ :=
  ∀ kn d, lookup_global Σ.(declarations) kn = Some d → GlobalEnvMap.lookup_env Σg kn = Some d.
Import ssreflect.

Lemma repr_lookup_constructor {Σg Σ} :
  repr_decls Σg Σ →
  ∀ ind idx r, lookup_constructor Σ ind idx = Some r → GlobalEnvMap.lookup_constructor Σg ind idx = Some r.
Proof.
  intros hrepr ind idx r.
  rewrite /lookup_constructor /lookup_constructor_gen /lookup_inductive /lookup_inductive_gen
          /lookup_minductive /lookup_minductive_gen /lookup_env.
  destruct lookup_global eqn:hl ⇒ //.
  apply hrepr in hl.
  rewrite /GlobalEnvMap.lookup_constructor /GlobalEnvMap.lookup_inductive /GlobalEnvMap.lookup_minductive hl //.
Qed.

Import bytestring.String.

Local Open Scope bs.

Lemma constructor_declared {cf : checker_flags} {Σ :global_env_ext} {Γ ind idx u ty} {wfΣ : wf Σ.1}:
  Σ ;;; Γ |- tConstruct ind idx u : ty →
  ∃ r, lookup_constructor Σ ind idx = Some r.
Proof.
  intros H; depind H; eauto.
  eexists. eapply declared_constructor_to_gen, declared_constructor_lookup_gen in isdecl; tea.
  Unshelve. all: eauto.
Qed.

Lemma eta_expand_expanded {cf : config.checker_flags} {Σ : global_env_ext} Γ Γ' t T :
  wf Σ →
  typing Σ Γ t T →
  Forall2 (fun x y ⇒ match x with Some (n, t) ⇒ y.(decl_type) = t ∧ context_assumptions (decompose_prod_assum [] y.(decl_type)).1 ≥ n | None ⇒ True end) Γ' Γ →
  ∀ Σg : GlobalEnvMap.t, repr_decls Σg Σ.1 →
  expanded Σ (map (fun x ⇒ match x with Some (n, _) ⇒ n | None ⇒ 0 end ) Γ') (eta_expand Σg Γ' t).
Proof.
  intros wf Hty. revert Γ'.
  eapply @typing_ind_env with (t := t) (Σ := Σ)
    (P := fun (Σ : global_env_ext) Γ t T ⇒ ∀ Γ', Forall2 (fun (x : option (nat × term)) (y : context_decl) ⇒
          match x with
        | Some (_, t0) ⇒ decl_type y = t0 ∧ _
        | None ⇒ True
        end) Γ' Γ →
  ∀ Σg, repr_decls Σg Σ.1 →
    expanded Σ (map (fun x : option (nat × term) ⇒
      match x with
      | Some (n, _) ⇒ n
      | None ⇒ 0
      end) Γ') (eta_expand Σg Γ' t))
    (Pj := fun (Σ : global_env_ext) Γ j ⇒ option_default (fun t ⇒ ∀ Γ', Forall2 (fun (x : option (nat × term)) (y : context_decl) ⇒
            match x with
          | Some (_, t0) ⇒ decl_type y = t0 ∧ _
          | None ⇒ True
          end) Γ' Γ →
      ∀ Σg, repr_decls Σg Σ.1 →
      expanded Σ (map (fun x : option (nat × term) ⇒
        match x with
        | Some (n, _) ⇒ n
        | None ⇒ 0
        end) Γ') (eta_expand Σg Γ' t)) (j_term j) True)
      (PΓ := fun _ _ _ ⇒ True);
    repeat match goal with
    | [ |- repr_decls _ _ → _ ] ⇒ intros hrepr
    | _ ⇒ intro
    end; try now (cbn; eauto).
  - apply fst in X. destruct j_term ⇒ //. apply snd in X. simpl. apply X.
  - cbn. eapply Forall2_nth_error_Some_r in H1 as (? & ? & ?); eauto.
    rewrite H1.
    destruct x as [[] | ].
    + destruct H2. unfold eta_single. cbn.
      eapply expanded_fold_lambda.
      rewrite !Nat.sub_0_r. len. rewrite length_firstn. len.
      destruct n0.
      × cbn. econstructor. now rewrite nth_error_map H1.
      × rewrite seq_S rev_map_spec map_app rev_app_distr. subst.
         rewrite <- context_assumptions_lift, !Nat.min_l; try lia.
        econstructor.
        -- rewrite nth_error_app2 repeat_length; try lia.
           replace (S n0 + n - S n0) with n by lia.
           now rewrite nth_error_map H1.
        -- len. now rewrite length_seq.
        -- eapply Forall_forall. intros x [ | (? & <- & [_ ?] % in_seq) % in_rev % in_map_iff]; subst.
           all: econstructor; rewrite nth_error_app1; revgoals; [eapply nth_error_repeat; lia | rewrite repeat_length; lia].
    + econstructor. now rewrite nth_error_map H1.
  - cbn. econstructor. eapply (H1 (up Γ')); tea; econstructor; eauto.
  - cbn. econstructor. eauto. eapply (H1 (up Γ')); tea; econstructor; eauto.
  - specialize (H _ H2).
    assert (Forall(fun t : term ⇒ expanded Σ0 (map
    (fun x : option (nat × term) ⇒
     match x with
     | Some p ⇒ let (n, _) := p in n
     | None ⇒ 0
     end) Γ') (eta_expand Σg Γ' t)) l). {
       clear H1. clear X. induction X0; econstructor; eauto. }
    destruct t0; cbn.
    all: try now eapply expanded_mkApps; [ eauto | solve_all ].
    + cbn in H.
      destruct (nth_error Γ' n) eqn:E; eauto.
      destruct o; eauto.
      destruct p. cbn in ×.
      eapply expanded_eta_single_tRel_app; eauto. solve_all.
      eapply Forall2_nth_error_Some_l in H2 as (? & ? & ?). 2: eauto.
      cbn in ×.
      destruct H4.
      rewrite <- context_assumptions_lift. subst. lia.
      cbn. eapply expanded_mkApps. constructor.
      now rewrite nth_error_map E; cbn.
      solve_all.
    + cbn in H. unfold eta_constructor in ×.
      specialize (H Σg hrepr).
      rewrite GlobalEnvMap.lookup_constructor_spec in H |- ×.
      destruct lookup_constructor as [[[mdecl idecl] cdecl]| ] eqn:E1; eauto.
      unfold eta_single in H. eapply expanded_fold_lambda.
      rewrite Nat.sub_0_r in H.
      unfold mkApps in H. destruct (ind_npars mdecl + context_assumptions (cstr_args cdecl)) eqn:EE.
      × cbn in H. inversion H; subst. cbn.
        simpl_list. destruct l.
        -- cbn. econstructor; eauto.
        -- cbn. eapply expanded_tConstruct_app; eauto. cbn. now rewrite H8.
           rewrite lift0_id. setoid_rewrite map_ext. 3: eapply lift0_p. rewrite map_id.
           eapply Forall_typing_spine_Forall in X0.
           rewrite <- map_cons. revert X0. generalize (t0 :: l). intros l' X0.
           solve_all. eapply H4; auto. solve_all. reflexivity.
      × eapply constructor_declared in X as [[[mdecl' idecl'] cdecl'] hc].
        have h := (repr_lookup_constructor hrepr _ _ _ hc). rewrite GlobalEnvMap.lookup_constructor_spec in h.
        rewrite E1 in h. noconf h.
        eapply expanded_mkApps_tConstruct. now eapply declared_constructor_from_gen, lookup_constructor_declared_gen.
        rewrite rev_map_spec. simpl_list. rewrite EE. lia. eapply Forall_typing_spine_Forall in X0.
        assert ((context_assumptions
        (decompose_prod_assum [] (type_of_constructor mdecl cdecl (ind, idx) u)).1) = ind_npars mdecl + context_assumptions (cstr_args cdecl)) as E. {
          eapply decompose_type_of_constructor; eauto.
          now eapply declared_constructor_from_gen, lookup_constructor_declared_gen. }
        eapply app_Forall.
        -- Opaque minus. solve_all. eapply @expanded_lift' with (Γ' := []). 2: reflexivity. reflexivity.
           2: reflexivity. len.
           { rewrite !length_firstn !List.length_skipn. len.
             rewrite E EE. lia.
           }
           cbn. eauto.
        -- rewrite rev_map_spec. eapply Forall_rev.
           eapply Forall_forall. intros ? (? & <- & ?) % in_map_iff. econstructor.
           eapply in_seq in H4 as [_ H4].
           len. rewrite nth_error_app1; len.
           rewrite !length_firstn !List.length_skipn. len. rewrite E EE.
           rewrite length_map in H4. lia.
           eapply nth_error_repeat. cbn in ×.
           rewrite !length_firstn !List.length_skipn. len. rewrite E EE.
           rewrite length_map in H4. lia.
    + specialize (H _ hrepr).
      cbn in H. unfold eta_fixpoint in ×.
      rewrite nth_error_map in H |- ×.
      destruct (nth_error mfix idx) eqn:Eid; eauto.
      cbn in ×.
      eapply expanded_fold_lambda.

      eapply expanded_mkApps_tFix; fold lift.
      2:{ rewrite !nth_error_map Eid. cbn. len. reflexivity. }
      ++ cbn. rewrite <- context_assumptions_lift.
        eapply wf_fixpoint_rarg; eauto. 2: eapply nth_error_In; eauto.
        clear - X. depind X; eauto.
      ++ len. rewrite length_seq. lia.
      ++ unfold eta_single in H.
         rewrite expanded_fold_lambda in H. cbn. simpl_list.
         cbn-[lift] in H. rewrite Nat.sub_0_r in H.
         unfold lift in H. fold lift in H.
         eapply expanded_mkApps_tFix_inv in H.
         eapply Forall_forall.
         intros ? (? & <- & (? & <- & ?) % in_map_iff) % in_map_iff. cbn.

         eapply Forall_forall in H. 2:{
         eapply in_map_iff. eexists. split. reflexivity. eapply in_map_iff. eexists. split. cbn. reflexivity. eauto. }
         cbn in H.
         revert H. len. intros [Hl H]. split.
         { eapply isLambda_unlift in Hl. now eapply isLambda_lift. }

         eapply typing_wf_fixpoint in X. eapply wf_fixpoint_rarg in X. 2: eauto. 2: eapply nth_error_In; eauto.

         assert (#|l| > S (rarg d) ∨ #|l| ≤ S (rarg d) ) as [He | He] by lia.
         { replace ((S (rarg d) - #|l|)) with 0 by lia. cbn. rewrite lift0_id.
          eapply expanded_unlift. 2: reflexivity.
          eapply apply_expanded; eauto; len. 2:{ f_equal. instantiate (1 := repeat 0 (S (rarg d))). now len. }
          simpl_list. rewrite !app_assoc. f_equal. f_equal.
          2:{ f_equal. rewrite !length_firstn. len.
              destruct context_assumptions; lia.
           }
          f_equal. rewrite !mapi_map. now eapply mapi_ext. }

         eapply expanded_unlift with (Γ'' := repeat 0 #|l|). 2: now rewrite <- app_assoc.
         rewrite → simpl_lift. 2:{ len. rewrite !length_firstn !List.length_skipn. lia. }
         2:{ len. lia. }
         eapply apply_expanded. eauto.
         simpl_list. f_equal. f_equal.
         ** rewrite !mapi_map. now eapply mapi_ext.
         ** rewrite !length_firstn !List.length_skipn.
            rewrite app_assoc. f_equal.
            rewrite <- repeat_app. f_equal. len.
            destruct context_assumptions;
            lia.
         ** f_equal. len. lia.
      ++ eapply Forall_typing_spine_Forall in X0. eapply app_Forall.
         ** solve_all. eapply @expanded_lift' with (Γ' := []). all: try now reflexivity. 2: eauto.
            len. rewrite !length_firstn !List.length_skipn.
            eapply typing_wf_fixpoint in X.
            eapply wf_fixpoint_rarg in X. 2: eauto. 2: eapply nth_error_In; eauto.
            len. lia.
         ** rewrite rev_map_spec. eapply Forall_rev.
            eapply Forall_forall. intros ? (? & <- & ?) % in_map_iff. econstructor.
            eapply in_seq in H4 as [_ H4]. autorewrite with len in H4 |- ×.
            rewrite !length_firstn !List.length_skipn.
            rewrite → nth_error_app1. eapply nth_error_repeat.
            -- len.
               eapply Nat.lt_le_trans. eauto. cbn.
               eapply typing_wf_fixpoint in X.
               eapply wf_fixpoint_rarg in X. 2: eauto. 2: eapply nth_error_In; eauto.
               lia.
            -- len.
               eapply Nat.lt_le_trans. eauto. cbn.
               eapply typing_wf_fixpoint in X.
               eapply wf_fixpoint_rarg in X. 2: eauto. 2: eapply nth_error_In; eauto.
               lia.
      ++ destruct l; cbn in *; try congruence.
      ++ cbn. eauto.
  - cbn. pose proof isdecl as isdecl'.
    unfold eta_constructor.
    eapply declared_constructor_to_gen, declared_constructor_lookup_gen in isdecl'.
    eapply (repr_lookup_constructor hrepr) in isdecl'. rewrite isdecl'.
    rewrite GlobalEnvMap.lookup_constructor_spec in isdecl'.
    eapply expanded_fold_lambda. rewrite Nat.sub_0_r.
    eapply expanded_mkApps_tConstruct; eauto.
    rewrite rev_map_spec. now simpl_list. rewrite rev_map_spec -!List.map_rev.
    eapply Forall_forall. intros ? (? & <- & ?) % in_map_iff. econstructor.
    eapply in_rev, in_seq in H2 as [_ ?]. cbn in ×. len.
    rewrite !length_firstn. len.
    assert ((context_assumptions
    (decompose_prod_assum []
       (type_of_constructor mdecl cdecl (ind, i) u)).1) = ind_npars mdecl + context_assumptions (cstr_args cdecl)) as →. {
      eapply decompose_type_of_constructor; eauto.
    }
    rewrite nth_error_app1. 2:now rewrite nth_error_repeat. rewrite repeat_length. lia.
  - cbn. econstructor; eauto.
    × unfold map_branches. solve_all.
      clear -hrepr X1 H8.
      set (Γ'' := map _ Γ'). cbn.
      enough (All (expanded Σ0 Γ'') (map (eta_expand Σg Γ') (pparams p ++ indices))).
      now rewrite map_app in X; eapply All_app in X as [].
      eapply All_map.
      induction X1.
      + constructor.
      + constructor; auto. eapply t1; solve_all; auto.
      + auto.

    × solve_all.
      specialize (b (repeat None #|bcontext y| ++ Γ'))%list.
      rewrite map_app map_repeat in b. eapply b; eauto.
      eapply Forall2_app; solve_all.

      assert (#| (case_branch_context_gen (ci_ind ci) mdecl (pparams p)
      (puinst p) (bcontext y) x)| = #|bcontext y|). { clear - a0.
        unfold case_branch_context_gen. rewrite map2_length.
        rewrite Nat.min_l; try lia. eapply All2_length in a0.
        unfold inst_case_context. unfold subst_context.
        unfold subst_instance, subst_instance_context, map_context.
        rewrite fold_context_k_length length_map. unfold aname. lia.
      } revert H9. generalize ((case_branch_context_gen (ci_ind ci) mdecl (pparams p)
      (puinst p) (bcontext y) x)). clear -hrepr.
      induction #|bcontext y|; intros []; cbn; intros; try congruence; econstructor; eauto.
    - cbn. rewrite nth_error_map H0. cbn. unfold eta_fixpoint. unfold fst_ctx in ×. cbn in ×.
    eapply expanded_fold_lambda.
    assert (#|(decompose_prod (dtype decl)).1.1| = #|(decompose_prod (dtype decl)).1.2|) as E1. { eapply decompose_prod12. }
    assert (rarg decl < context_assumptions (decompose_prod_assum [] (dtype decl)).1) as E2. { eapply wf_fixpoint_rarg; eauto. now eapply nth_error_In. }
    eapply expanded_mkApps_tFix.
    + shelve.
    + fold lift. rewrite !nth_error_map H0. cbn. len. reflexivity.
    + len. rewrite length_seq. lia.
    + fold lift. len.
      assert (Forall (fun x ⇒ isLambda (dbody x)) mfix).
      { apply andb_and in H2. destruct H2 as [isl _]. solve_all. }
      solve_all.
      { now eapply isLambda_lift, isLambda_eta_expand. }
      cbn in ×.
      rewrite !length_firstn. rewrite → !Nat.min_l; try lia.
      eapply expanded_lift'.
      5: eapply a2; eauto. 2: reflexivity. 2: now len.
      2: now len.
      { rewrite map_app. f_equal. rewrite map_rev. f_equal. now rewrite !mapi_map map_mapi. }
      eapply Forall2_app; solve_all.
      subst types. unfold Typing.fix_context.
      eapply All2_rev. eapply All2_mapi. eapply All_All2_refl, Forall_All, Forall_forall.
      intros. split. reflexivity. cbn.
      rewrite <- context_assumptions_lift.
      eapply wf_fixpoint_rarg in H4; eauto. len; lia.
      Unshelve. all: eauto. cbn. rewrite <- context_assumptions_lift. lia.
    + cbn - [rev_map seq]. rewrite rev_map_spec. eapply Forall_rev.
      eapply Forall_forall. intros ? (? & <- & ?) % in_map_iff. econstructor.
      eapply in_seq in H4 as [_ ?]. cbn in ×. len.
      rewrite !length_firstn.
      rewrite → nth_error_app1. eapply nth_error_repeat.
      len; lia.
      rewrite repeat_length. len; lia.
    + cbn - [rev_map seq]. rewrite rev_map_spec. cbn. rewrite Nat.sub_0_r. cbn. destruct List.rev; cbn; congruence.
  - cbn. econstructor; eauto. eapply All_Forall, All_map, All_impl with (1 := X2). cbn. intros ? e0.
     specialize (e0 (repeat None #|mfix| ++ Γ'))%list.
     rewrite map_app map_repeat in e0. len. eapply e0; auto.
     eapply Forall2_app; eauto. unfold types.
     assert (#|Typing.fix_context mfix| = #|mfix|). { unfold Typing.fix_context. now len. }
     revert H4. generalize (Typing.fix_context mfix). clear.
     induction #|mfix|; intros []; cbn; intros; try congruence; econstructor; eauto.
  - cbn. econstructor; eauto. solve_all. eapply b; tea. solve_all.
  - eapply typing_wf_local; eauto.
Qed.

Arguments tVar _%_bs.

From Stdlib Require Import ssreflect.
Open Scope bs_scope.

Fixpoint lookup_global_env (Σ : global_declarations) (kn : kername) {struct Σ} : option (global_decl × global_declarations) :=
  match Σ with
  | [] ⇒ None
  | d :: tl ⇒ if kn == d.1 then Some (d.2, tl) else lookup_global_env tl kn
  end.

Lemma lookup_lookup_global_env Σ kn decl :
  lookup_global Σ kn = Some decl → ∑ Σ', lookup_global_env Σ kn = Some (decl, Σ').
Proof.
  induction Σ ⇒ // /=.
  case: eqb_specT ⇒ eq.
  intros [= <-]. subst kn.
  now eexists.
  auto.
Qed.

Lemma lookup_global_env_lookup Σ kn dΣ :
  lookup_global_env Σ kn = Some dΣ → lookup_global Σ kn = Some dΣ.1.
Proof.
  induction Σ ⇒ // /=.
  case: eqb_specT ⇒ eq.
  intros [= <-]. subst kn.
  reflexivity.
  auto.
Qed.

Lemma lookup_lookup_global_env_None Σ kn :
  lookup_global Σ kn = None ↔ lookup_global_env Σ kn = None.
Proof.
  induction Σ ⇒ // /=.
  case: eqb_specT ⇒ eq //.
Qed.

Lemma eta_lookup_global {Σ : GlobalEnvMap.t} kn decl :
  lookup_env Σ kn = Some decl →
  lookup_global (eta_global_declarations Σ Σ.(declarations)) kn = Some (eta_global_declaration Σ decl).
Proof.
  move/lookup_lookup_global_env ⇒ [] Σ' hl.
  move: hl.
  induction (declarations Σ); cbn ⇒ //.
  destruct a as [kn' []] ⇒ /=.
  case: eqb_spec. intros →. intros [= <- <-] ⇒ //.
  intros neq. auto.
  case: eqb_spec. intros →. intros [= <- <-] ⇒ //.
  intros neq. auto.
Qed.

Lemma lookup_global_map_on_snd f decls kn : lookup_global (map (on_snd f) decls) kn = option_map f (lookup_global decls kn).
Proof.
  induction decls; cbn ⇒ //.
  case: eqb_spec.
  - now intros →.
  - now intros neq.
Qed.

Lemma eta_lookup_global_error Σ ind :
   lookup_global (eta_global_declarations Σ Σ.(declarations)) (inductive_mind ind) = None →
   lookup_global Σ.(declarations) (inductive_mind ind) = None.
Proof.
  unfold eta_global_declarations.
  rewrite lookup_global_map_on_snd. destruct lookup_global ⇒ //.
Qed.

Lemma eta_declared_constructor {cf:checker_flags} {Σ : GlobalEnvMap.t}
  {wfΣ : wf Σ} {ind mdecl idecl cdecl} :
  declared_constructor Σ ind mdecl idecl cdecl →
  declared_constructor (eta_expand_global_env Σ) ind (eta_minductive_decl Σ mdecl)
    (eta_inductive_decl Σ mdecl idecl) (eta_constructor_decl Σ mdecl cdecl).
Proof.
  intros H. eapply declared_constructor_from_gen.
  eapply declared_constructor_to_gen in H.
  destruct H as [[] ?].
  move: H.
  rewrite /declared_inductive /declared_inductive_gen /declared_minductive /declared_minductive_gen
         /lookup_env /=.
  destruct (lookup_global Σ.(declarations) _) eqn:heq ⇒ //.
  move: (eta_lookup_global (inductive_mind ind.1) g heq) ⇒ hl.
  intros [= ->].
  unfold declared_constructor_gen, declared_inductive_gen, declared_minductive_gen.
  rewrite hl; split ⇒ //.
  split ⇒ //. rewrite nth_error_map H0 //.
  rewrite nth_error_map H1 //.
  Unshelve. all: eauto.
Qed.

Import ssreflect ssrbool.

Definition same_cstr_info Σ Σ' :=
  ∀ ind idx mdecl idecl cdecl,
  declared_constructor Σ (ind, idx) mdecl idecl cdecl →
  ∃ mdecl' idecl' cdecl',
    [/\ declared_constructor Σ' (ind, idx) mdecl' idecl' cdecl',
    mdecl.(ind_npars) = mdecl'.(ind_npars) &
    context_assumptions cdecl.(cstr_args) = context_assumptions cdecl'.(cstr_args)].

Lemma expanded_env_irrel Σ Σ' Γ t :
  same_cstr_info Σ Σ' →
  expanded Σ Γ t →
  expanded Σ' Γ t.
Proof.
  intros hrepr.
  induction 1 using expanded_ind.
  all: try solve [constructor; auto].
  - eapply expanded_tRel_app; tea.
  - eapply hrepr in H as [mdecl' [idecl' [cdecl' [hdecl hpars hass]]]].
    eapply expanded_tConstruct; tea. lia.
  - eapply expanded_tFix; tea. solve_all.
  - eapply hrepr in H as [mdecl' [idecl' [cdecl' [hdecl hpars hass]]]].
    eapply expanded_tConstruct_app; tea. cbn. lia.
Qed.

Lemma expanded_context_env_irrel Σ Σ' Γ t :
  same_cstr_info Σ Σ' →
  expanded_context Σ Γ t →
  expanded_context Σ' Γ t.
Proof.
  unfold expanded_decl.
  unfold expanded_context.
  intros hrepr []; split. eapply All_fold_impl; tea; cbn ⇒ ?? []; constructor.
  eapply expanded_env_irrel; tea.
Qed.

Lemma expanded_decl_env_irrel (Σ Σ' : global_env) t :
  same_cstr_info Σ Σ' →
  expanded_decl Σ t →
  expanded_decl Σ' t.
Proof.
  intros hrepr.
  unfold expanded_decl.
  destruct t ⇒ //.
  intros []. constructor.
  destruct (cst_body c) ⇒ //. cbn in ×.
  now eapply expanded_env_irrel.
  intros []. split.
  eapply expanded_context_env_irrel; tea.
  solve_all.
  destruct H. constructor.
  solve_all. destruct H; split.
  eapply expanded_context_env_irrel; tea.
  eapply expanded_env_irrel; tea.
Qed.

Coercion wf_ext_wf : wf_ext >-> wf.
Implicit Types (cf : checker_flags).
Lemma All_fold_fold_context_k_defs P (f : nat → term → term) Γ :
  All_fold P (fold_context_k_defs f Γ) <~>
  All_fold (fun Γ d ⇒ P (fold_context_k_defs f Γ) (map_decl_body (f #|Γ|) d)) Γ.
Proof.
  split.
  - induction Γ; auto.
    × intros; constructor.
    × cbn. intros H; depelim H. constructor; auto.
  - induction Γ; auto.
    × intros; constructor.
    × intros H; depelim H. constructor; auto.
Qed.

#[export] Hint Rewrite @fold_context_k_defs_length @context_assumptions_fold_context_k_defs : len.

Existing Class Typing.wf_ext.

Definition global_env_ext_map := GlobalEnvMap.t × universes_decl.

Definition global_env_ext_map_global_env_map (Σgext : global_env_ext_map) : GlobalEnvMap.t := Σgext.1.

Definition global_env_ext_map_global_env_ext (Σgext : global_env_ext_map) : global_env_ext :=
  (Σgext.1.(GlobalEnvMap.env), Σgext.2).

Coercion global_env_ext_map_global_env_map : global_env_ext_map >-> GlobalEnvMap.t.
Coercion global_env_ext_map_global_env_ext : global_env_ext_map >-> global_env_ext.

Lemma repr_global_env_map (Σ : GlobalEnvMap.t) : repr_decls Σ Σ.
Proof.
  destruct Σ as [].
  unfold repr_decls.
  intros kn d.
  cbn. rewrite GlobalEnvMap.lookup_env_spec. now cbn.
Qed.

Lemma eta_expand_context {cf} {Σ} {Σg : global_env_ext_map} {ctx} {wfΣ : Typing.wf_ext Σ} :
  repr_decls Σg Σ →
  on_context (lift_typing typing) Σ ctx →
  expanded_context Σ [] (eta_context Σg 0 ctx).
Proof.
  unfold on_context.
  red. intros hrepr wf. sq.
  rewrite /eta_context.
  eapply All_fold_fold_context_k_defs.
  induction wf; cbn; auto; try constructor; auto.
  cbn. constructor.
  cbn. constructor.
  len. rewrite app_nil_r.
  destruct t1 as (t1 & s & t2 & _).
  cbn in t1, t2.
  forward (eta_expand_expanded (Σ := Σ) Γ (repeat None #|Γ|) _ _ wfΣ t1).
  clear. induction Γ; cbn; constructor; auto.
  intros. specialize (H _ hrepr).
  move: H.
  now rewrite map_repeat.
Qed.

Lemma eta_expand_context_sorts {cf} {Σ} {Σg : global_env_ext_map} {ctx ctx' cunivs} {wfΣ : Typing.wf_ext Σ} :
  repr_decls Σg Σ →
  sorts_local_ctx (lift_typing typing) Σ ctx ctx' cunivs →
  expanded_context Σ (repeat 0 #|ctx|) (eta_context Σg #|ctx| ctx').
Proof.
  intros hrepr hs. constructor.
  eapply All_fold_fold_context_k_defs. cbn. len.
  induction ctx' in hs, cunivs |- *; cbn; auto.
  constructor; eauto.
  cbn in hs. destruct a as [na [b|] ty]; try destruct hs as [hs ?].
  specialize (IHctx' cunivs hs). constructor; auto.
  constructor. len. rewrite repeat_app.
  destruct l as [Htm [s Hs]].
  epose proof (eta_expand_expanded (Σ := Σ) _ (repeat None (#|ctx'| + #|ctx|)) _ _ wfΣ Htm).
  forward H.
  clear. rewrite -app_context_length.
  induction (_ ,,, _); cbn; constructor; auto.
  specialize (H _ hrepr).
  now rewrite map_repeat !repeat_app in H.
  destruct cunivs ⇒ //. destruct hs.
  constructor; eauto. constructor.
Qed.

Lemma eta_context_length g n ctx : #|eta_context g n ctx| = #|ctx|.
Proof. now rewrite /eta_context; len. Qed.
#[export] Hint Rewrite @eta_context_length : len.

Lemma eta_expand_global_decl_expanded {cf : checker_flags} (Σ : global_env_ext) (Σg : global_env_ext_map) kn d :
  repr_decls Σg Σ →
  Typing.wf_ext Σ →
  on_global_decl cumul_gen (lift_typing typing) Σ kn d →
  expanded_decl Σ (eta_global_declaration Σg d).
Proof.
  intros hrepr wf ond.
  destruct d; cbn in ×.
  - unfold on_constant_decl in ond.
    destruct c as [na body ty rel]; cbn in ×.
    destruct body. constructor ⇒ //; cbn.
    apply (eta_expand_expanded (Σ := Σ) [] [] t0 na wf ond.1). constructor.
    apply hrepr.
    destruct ond as [s Hs]. constructor ⇒ //.
  - destruct ond as [onI onP onN onV].
    constructor. cbn.
    eapply eta_expand_context ⇒ //.
    solve_all. cbn. eapply All_map, Alli_All; tea ⇒ n idecl oni.
    constructor.
    cbn. solve_all.
    pose proof oni.(onConstructors).
    red in X.
    eapply All2_All_left; tea; cbn ⇒ cdecl cunivs onc.
    constructor. cbn. len.
    pose proof onc.(on_cargs).
    eapply eta_expand_context_sorts in X0. now len in X0. exact hrepr.
    len. len.
    pose proof onc.(on_ctype). destruct X0 as (_ & s & t0 & _).
    epose proof (eta_expand_expanded (Σ := Σ) _ (repeat None #|ind_bodies m|) _ _ wf t0).
    forward H. rewrite -arities_context_length.
    clear. induction (arities_context _); constructor; auto.
    specialize (H _ hrepr).
    now rewrite map_repeat in H.
Qed.

Lemma eta_context_assumptions Σ n Γ : context_assumptions Γ = context_assumptions (eta_context Σ n Γ).
Proof.
  now rewrite /eta_context context_assumptions_fold_context_k_defs.
Qed.

Lemma same_cstr_info_eta {cf:checker_flags} (Σ : global_env) {wfΣ : wf Σ} (Σg: GlobalEnvMap.t) :
  same_cstr_info Σ
    {| universes := Σ.(universes) ;
       declarations := List.map (on_snd (eta_global_declaration Σg)) Σ.(declarations);
       retroknowledge := Σ.(retroknowledge) |}.
Proof.
  destruct Σ as [univs Σ]; cbn.
  induction Σ; intros ind idx mdecl idecl cdecl.
  - unfold declared_constructor, declared_inductive, declared_minductive.
    cbn ⇒ [[[]]] //.
  - rewrite /declared_constructor.
    intros [[H hnth] hnth'].
    eapply declared_minductive_to_gen, declared_minductive_lookup_gen in H; eauto. move:H.
    rewrite /lookup_inductive /lookup_inductive_gen /lookup_minductive /lookup_minductive_gen
            /lookup_env /=.
    destruct a as [kn decl]; cbn.
    case: eqb_spec.
    × destruct decl ⇒ //.
      intros Hind Hm. inversion Hm.
      do 3 eexists; cbn. split. split. split ⇒ //.
      apply lookup_global_Some_if_In; cbn.
      subst. case: eqb_spec⇒ //.
      cbn. rewrite nth_error_map hnth; reflexivity.
      cbn. rewrite nth_error_map hnth'; reflexivity.
      now cbn. cbn. apply eta_context_assumptions.
    × intros Hind Hm.
      red in IHΣ.
      assert (wfΣ' : wf
      {|
        universes := univs;
        declarations := Σ;
        retroknowledge := retroknowledge0
      |}).
      { destruct wfΣ; econstructor =>//.
        inversion o0 =>//. }
      specialize (IHΣ wfΣ' ind idx mdecl idecl cdecl).
      forward IHΣ. repeat split ⇒ //.
      unfold declared_minductive.
      apply lookup_global_Some_if_In; cbn.
      move :Hm. destruct (lookup_global _ _) ⇒ //.
      destruct g =>//. intro H; inversion H; now subst.
      clear - cf wfΣ wfΣ' IHΣ Hind. destruct IHΣ as [mdecl' [idecl' [cdecl' [[[H ?] ?] ?]]]].
      ∃ mdecl', idecl', cdecl'. repeat split ⇒ //.
      cbn in ×. right. exact H.
      Unshelve. all: eauto.
Qed.

Lemma lookup_global_Some_fresh Σ c decl :
  lookup_global Σ c = Some decl → ¬ (fresh_global c Σ).
Proof.
  induction Σ; cbn. 1: congruence.
  destruct (eqb_spec c a.1); subst.
  - intros [= <-] H2. inv H2.
    contradiction.
  - intros H1 H2. apply IHΣ; tas.
    now inv H2.
Qed.

Lemma lookup_env_Some_fresh Σ c decl :
  lookup_env Σ c = Some decl → ¬ (fresh_global c Σ.(declarations)).
Proof.
  apply lookup_global_Some_fresh.
Qed.

Lemma lookup_global_extends Σ Σ' kn d :
  lookup_env Σ kn = Some d →
  extends Σ Σ' →
  EnvMap.fresh_globals Σ'.(declarations) →
  lookup_env Σ' kn = Some d.
Proof.
  setoid_rewrite EnvMap.fresh_globals_iff_NoDup.
  intros; eapply lookup_env_extends_NoDup; tea.
Qed.

Lemma eta_expand_global_env_expanded {cf : checker_flags} (Σ : global_env_ext_map) :
  Typing.wf Σ →
  expanded_global_env (eta_expand_global_env Σ).
Proof.
  destruct Σ as [Σ univs]; cbn.
  unfold expanded_global_env. cbn.
  unfold Typing.wf, Typing.on_global_env. intros [onu ond].
  cbn in ×.
  destruct Σ as []. cbn in ×.
  assert (strictly_extends_decls env env) by reflexivity.
  revert X.
  move: map repr wf.
  generalize env at 1 2 4 6 7.
  destruct env as [univs' decls retro']. cbn in ×.
  induction ond; cbn; constructor; auto.
  apply: IHond.
  { cbn. destruct X as [equ [Σ' ext]]. red. split. auto.
    rewrite ext. cbn. unfold snoc. ∃ (Σ' ++ [(kn, d)])%list. now rewrite -app_assoc.
    apply e. }
  set (Σ' := {| universes := univs'; declarations := Σ; retroknowledge := retro' |}) in ×.
  set (Σg := {| GlobalEnvMap.env := _ |}). Unshelve.
  destruct X as [equ [Σ'' ext]]. cbn in ×. destruct env as [univs0 env]. cbn in ×. subst univs0.
  subst env. destruct o as [? udecl ? o0].
  pose proof (eta_expand_global_decl_expanded (Σ', udecl) (Σg, univs) kn d).
  cbn in H.
  forward H. {
    move⇒ kn' d' /= hl.
    rewrite GlobalEnvMap.lookup_env_spec /=.
    cbn. unfold snoc.
    eapply (lookup_global_extends Σ' (set_declarations Σ' (Σ'' ++ (kn, d) :: Σ)%list)); eauto.
    apply extends_decls_extends, strictly_extends_decls_extends_decls.
    split ⇒ //. cbn. now ∃ (Σ'' ++ [(kn, d)])%list; rewrite -app_assoc. }
  forward H. split. cbn. split ⇒ //. now cbn.
  specialize (H o0).
  eapply expanded_decl_env_irrel in H; tea.
  eapply (same_cstr_info_eta Σ' Σg).
  Unshelve. all: eauto. econstructor =>//.
Qed.