(* Distributed under the terms of the MIT license. *)
From Coq Require Import CRelationClasses.
From Equations.Type Require Import Relation Relation_Properties.
From MetaCoq.Utils Require Import utils.
From MetaCoq.Common Require Import config BasicAst Reflect.
From MetaCoq.PCUIC Require Import PCUICAst PCUICOnOne PCUICAstUtils PCUICEquality
     PCUICLiftSubst PCUICUnivSubst PCUICCases PCUICOnFreeVars.

Set Default Goal Selector "!".

Implicit Types (cf : checker_flags).

Definition cumul_predicate (cumul : context → term → term → Type) Γ Re p p' :=
  All2 (cumul Γ) p.(pparams) p'.(pparams) ×
  (R_universe_instance Re p.(puinst) p'.(puinst) ×
  ((eq_context_gen eq eq p.(pcontext) p'.(pcontext)) ×
    cumul (Γ ,,, inst_case_predicate_context p) p.(preturn) p'.(preturn))).

Definition cumul_predicate_dep {cumul Γ Re p p'}
  (H : cumul_predicate cumul Γ Re p p')
  (cumul' : ∀ Γ p p', cumul Γ p p' → Type)
  Re'
  :=
  let '(Hparams, (Huinst, (Heq, Hcumul))) := H in
  All2_dep (cumul' Γ) Hparams ×
    (R_universe_instance_dep Re Re' Huinst
     × cumul' _ _ _ Hcumul).

Lemma cumul_predicate_undep {cumul Γ Re p p' H cumul' Re'}
  : @cumul_predicate cumul' Γ Re' p p' <~> @cumul_predicate_dep cumul Γ Re p p' H (fun Γ p p' _ ⇒ cumul' Γ p p') (fun x y _ ⇒ Re' x y).
Proof.
  cbv [cumul_predicate cumul_predicate_dep R_universe_instance R_universe_instance_dep] in ×.
  split; intro; repeat destruct ?; subst; rdest; try assumption.
  all: repeat first [ assumption | toAll ].
Qed.

Reserved Notation " Σ ;;; Γ ⊢ t ≤s[ pb ] u" (at level 50, Γ, t, u at next level,
  format "Σ ;;; Γ ⊢ t ≤s[ pb ] u").

Definition cumul_Ind_univ {cf} (Σ : global_env_ext) pb i napp :=
  R_global_instance Σ (eq_universe Σ) (compare_universe pb Σ) (IndRef i) napp.

Definition cumul_Construct_univ {cf} (Σ : global_env_ext) pb i k napp :=
  R_global_instance Σ (eq_universe Σ) (compare_universe pb Σ) (ConstructRef i k) napp.

Local Unset Elimination Schemes.
Inductive cumulSpec0 {cf : checker_flags} (Σ : global_env_ext) Γ (pb : conv_pb) : term → term → Type :=

(* transitivity *)

| cumul_Trans : ∀ t u v,
    is_closed_context Γ → is_open_term Γ u →
    Σ ;;; Γ ⊢ t ≤s[pb] u →
    Σ ;;; Γ ⊢ u ≤s[pb] v →
    Σ ;;; Γ ⊢ t ≤s[pb] v

(* symmetry *)

| cumul_Sym : ∀ t u,
    Σ ;;; Γ ⊢ t ≤s[Conv] u →
    Σ ;;; Γ ⊢ u ≤s[pb] t

(* reflexivity *)

| cumul_Refl : ∀ t,
    Σ ;;; Γ ⊢ t ≤s[pb] t

(* Cumulativity rules *)

| cumul_Ind : ∀ i u u' args args',
    cumul_Ind_univ Σ pb i #|args| u u' →
    All2 (fun t u ⇒ Σ ;;; Γ ⊢ t ≤s[Conv] u) args args' →
    Σ ;;; Γ ⊢ mkApps (tInd i u) args ≤s[pb] mkApps (tInd i u') args'

| cumul_Construct : ∀ i k u u' args args',
    cumul_Construct_univ Σ pb i k #|args| u u' →
    All2 (fun t u ⇒ Σ ;;; Γ ⊢ t ≤s[Conv] u) args args' →
    Σ ;;; Γ ⊢ mkApps (tConstruct i k u) args ≤s[pb] mkApps (tConstruct i k u') args'

| cumul_Sort : ∀ s s',
    compare_universe pb Σ s s' →
    Σ ;;; Γ ⊢ tSort s ≤s[pb] tSort s'

| cumul_Const : ∀ c u u',
    R_universe_instance (compare_universe Conv Σ) u u' →
    Σ ;;; Γ ⊢ tConst c u ≤s[pb] tConst c u'

(* congruence rules *)

| cumul_Evar : ∀ e args args',
    All2 (fun t u ⇒ Σ ;;; Γ ⊢ t ≤s[Conv] u) args args' →
    Σ ;;; Γ ⊢ tEvar e args ≤s[pb] tEvar e args'

| cumul_App : ∀ t t' u u',
    Σ ;;; Γ ⊢ t ≤s[pb] t' →
    Σ ;;; Γ ⊢ u ≤s[Conv] u' →
    Σ ;;; Γ ⊢ tApp t u ≤s[pb] tApp t' u'

| cumul_Lambda : ∀ na na' ty ty' t t',
    eq_binder_annot na na' →
    Σ ;;; Γ ⊢ ty ≤s[Conv] ty' →
    Σ ;;; Γ ,, vass na ty ⊢ t ≤s[pb] t' →
    Σ ;;; Γ ⊢ tLambda na ty t ≤s[pb] tLambda na' ty' t'

| cumul_Prod : ∀ na na' a a' b b',
    eq_binder_annot na na' →
    Σ ;;; Γ ⊢ a ≤s[Conv] a' →
    Σ ;;; Γ ,, vass na a ⊢ b ≤s[pb] b' →
    Σ ;;; Γ ⊢ tProd na a b ≤s[pb] tProd na' a' b'

| cumul_LetIn : ∀ na na' t t' ty ty' u u',
    eq_binder_annot na na' →
    Σ ;;; Γ ⊢ t ≤s[Conv] t' →
    Σ ;;; Γ ⊢ ty ≤s[Conv] ty' →
    Σ ;;; Γ ,, vdef na t ty ⊢ u ≤s[pb] u' →
    Σ ;;; Γ ⊢ tLetIn na t ty u ≤s[pb] tLetIn na' t' ty' u'

| cumul_Case indn : ∀ p p' c c' brs brs',
    cumul_predicate (fun Γ t u ⇒ Σ ;;; Γ ⊢ t ≤s[Conv] u) Γ (compare_universe Conv Σ) p p' →
    Σ ;;; Γ ⊢ c ≤s[Conv] c' →
    All2 (fun br br' ⇒
      eq_context_gen eq eq (bcontext br) (bcontext br') ×
      Σ ;;; Γ ,,, inst_case_branch_context p br ⊢ bbody br ≤s[Conv] bbody br'
    ) brs brs' →
    Σ ;;; Γ ⊢ tCase indn p c brs ≤s[pb] tCase indn p' c' brs'

| cumul_Proj : ∀ p c c',
    Σ ;;; Γ ⊢ c ≤s[Conv] c' →
    Σ ;;; Γ ⊢ tProj p c ≤s[pb] tProj p c'

| cumul_Fix : ∀ mfix mfix' idx,
    All2 (fun x y ⇒
      Σ ;;; Γ ⊢ x.(dtype) ≤s[Conv] y.(dtype) ×
      Σ ;;; Γ ,,, fix_context mfix ⊢ x.(dbody) ≤s[Conv] y.(dbody) ×
      (x.(rarg) = y.(rarg)) ×
      eq_binder_annot x.(dname) y.(dname)
    ) mfix mfix' →
    Σ ;;; Γ ⊢ tFix mfix idx ≤s[pb] tFix mfix' idx

| cumul_CoFix : ∀ mfix mfix' idx,
    All2 (fun x y ⇒
      Σ ;;; Γ ⊢ x.(dtype) ≤s[Conv] y.(dtype) ×
      Σ ;;; Γ ,,, fix_context mfix ⊢ x.(dbody) ≤s[Conv] y.(dbody) ×
      (x.(rarg) = y.(rarg)) ×
      eq_binder_annot x.(dname) y.(dname)
    ) mfix mfix' →
    Σ ;;; Γ ⊢ tCoFix mfix idx ≤s[pb] tCoFix mfix' idx

| cumul_beta : ∀ na t b a,
    Σ ;;; Γ ⊢ tApp (tLambda na t b) a ≤s[pb] b {0 := a}

| cumul_zeta : ∀ na b t b',
    Σ ;;; Γ ⊢ tLetIn na b t b' ≤s[pb] b' {0 := b}

| cumul_rel i body :
    option_map decl_body (nth_error Γ i) = Some (Some body) →
    Σ ;;; Γ ⊢ tRel i ≤s[pb] lift0 (S i) body

| cumul_iota : ∀ ci c u args p brs br,
    nth_error brs c = Some br →
    #|args| = (ci.(ci_npar) + context_assumptions br.(bcontext))%nat →
    Σ ;;; Γ ⊢ tCase ci p (mkApps (tConstruct ci.(ci_ind) c u) args) brs ≤s[pb] iota_red ci.(ci_npar) p args br

| cumul_fix : ∀ mfix idx args narg fn,
    unfold_fix mfix idx = Some (narg, fn) →
    is_constructor narg args = true →
    Σ ;;; Γ ⊢ mkApps (tFix mfix idx) args ≤s[pb] mkApps fn args

| cumul_cofix_case : ∀ ip p mfix idx args narg fn brs,
    unfold_cofix mfix idx = Some (narg, fn) →
    Σ ;;; Γ ⊢ tCase ip p (mkApps (tCoFix mfix idx) args) brs ≤s[pb] tCase ip p (mkApps fn args) brs

| cumul_cofix_proj : ∀ p mfix idx args narg fn,
    unfold_cofix mfix idx = Some (narg, fn) →
    Σ ;;; Γ ⊢ tProj p (mkApps (tCoFix mfix idx) args) ≤s[pb] tProj p (mkApps fn args)

| cumul_delta : ∀ c decl body (isdecl : declared_constant Σ c decl) u,
    decl.(cst_body) = Some body →
    Σ ;;; Γ ⊢ tConst c u ≤s[pb] body@[u]

| cumul_proj : ∀ p args u arg,
    nth_error args (p.(proj_npars) + p.(proj_arg)) = Some arg →
    Σ ;;; Γ ⊢ tProj p (mkApps (tConstruct p.(proj_ind) 0 u) args) ≤s[pb] arg

where " Σ ;;; Γ ⊢ t ≤s[ pb ] u " := (@cumulSpec0 _ Σ Γ pb t u) : type_scope.

Definition convSpec `{checker_flags} (Σ : global_env_ext) Γ := cumulSpec0 Σ Γ Conv.
Definition cumulSpec `{checker_flags} (Σ : global_env_ext) Γ := cumulSpec0 Σ Γ Cumul.

(* ** Syntactic cumulativity up-to universes *)

Notation " Σ ;;; Γ |- t <=s u " := (@cumulSpec _ Σ Γ t u) (at level 50, Γ, t, u at next level).
Notation " Σ ;;; Γ |- t =s u " := (@convSpec _ Σ Γ t u) (at level 50, Γ, t, u at next level).

Include PCUICConversion.

Module PCUICConversionParSpec <: EnvironmentTyping.ConversionParSig PCUICTerm PCUICEnvironment PCUICTermUtils PCUICEnvTyping.
  Definition cumul_gen := @cumulSpec0.
End PCUICConversionParSpec.

Notation " Σ ⊢ Γ ≤s[ pb ] Δ " := (@cumul_pb_context _ pb Σ Γ Δ) (at level 50, Γ, Δ at next level) : type_scope.
Notation " Σ ⊢ Γ ≤s Δ " := (@cumul_pb_context _ Cumul Σ Γ Δ) (at level 50, Γ, Δ at next level) : type_scope.
Notation " Σ ⊢ Γ =s Δ " := (@cumul_pb_context _ Conv Σ Γ Δ) (at level 50, Γ, Δ at next level) : type_scope.

#[global]
Instance cumul_spec_refl {cf:checker_flags} Σ Γ pb : Reflexive (cumulSpec0 Σ Γ pb).
Proof. intro; constructor 3. Qed.

#[global]
Instance conv_refl' {cf:checker_flags} Σ Γ : Reflexive (convSpec Σ Γ) := _.

#[global]
Instance cumul_pb_decls_refl {cf:checker_flags} pb Σ Γ Γ' : Reflexive (cumul_pb_decls cumulSpec0 pb Σ Γ Γ').
Proof.
  intros x. destruct x as [na [b|] ty]; constructor; auto.
  all:constructor; reflexivity.
Qed.

#[global]
Instance conv_decls_refl {cf:checker_flags} Σ Γ Γ' : Reflexive (conv_decls cumulSpec0 Σ Γ Γ') := _.
#[global]
Instance cumul_decls_refl {cf:checker_flags} Σ Γ Γ' : Reflexive (cumul_decls cumulSpec0 Σ Γ Γ') := _.

Section ContextConversion.
  Context {cf : checker_flags}.
  Context (Σ : global_env_ext).

  Notation conv_context := (conv_context cumulSpec0 Σ).
  Notation cumul_context := (cumul_context cumulSpec0 Σ).

  Global Instance cumul_pb_ctx_refl pb : Reflexive (cumul_pb_context cumulSpec0 pb Σ).
  Proof using Type.
    intro Γ; induction Γ; try econstructor; auto.
    reflexivity.
  Qed.

  Global Instance conv_ctx_refl : Reflexive (conv_context) := _.
  Global Instance cumul_ctx_refl : Reflexive (cumul_context) := _.

  Definition conv_ctx_refl' Γ : conv_context Γ Γ
  := conv_ctx_refl Γ.

  Definition cumul_ctx_refl' Γ : cumul_context Γ Γ
    := cumul_ctx_refl Γ.

End ContextConversion.

Lemma cumulSpec0_rect :
  ∀ cf (Σ : global_env_ext)
         (P : ∀ cf Σ Γ pb u v, @cumulSpec0 cf Σ Γ pb u v → Type),

    (* beta *)
    (∀ (Γ : context) (pb : conv_pb) (na : aname) (t b a : term),
        P cf Σ Γ pb (tApp (tLambda na t b) a) (b {0 := a}) (cumul_beta _ _ _ _ _ _ _)) →

    (* let *)
    (∀ (Γ : context) (pb : conv_pb) (na : aname) (b t b' : term),
        P cf Σ Γ pb (tLetIn na b t b') (b' {0 := b}) (cumul_zeta _ _ _ _ _ _ _)) →

    (∀ (Γ : context) (pb : conv_pb) (i : nat) (body : term)
            (pf : option_map decl_body (nth_error Γ i) = Some (Some body)),
        P cf Σ Γ pb (tRel i) ((lift0 (S i)) body) (cumul_rel _ _ _ _ _ pf)) →

    (* iota *)
    (∀ (Γ : context) (pb : conv_pb) (ci : case_info) (c : nat) (u : Instance.t) (args : list term)
            (p : predicate term) (brs : list (branch term)) br
            (Hbrs : nth_error brs c = Some br)
            (Hnargs : #|args| = (ci.(ci_npar) + context_assumptions br.(bcontext))%nat),
        P cf Σ Γ pb (tCase ci p (mkApps (tConstruct ci.(ci_ind) c u) args) brs)
          (iota_red ci.(ci_npar) p args br)
          (cumul_iota _ _ _ _ _ _ _ _ _ _ Hbrs Hnargs)) →

    (* fix unfolding *)
    (∀ (Γ : context) (pb : conv_pb) (mfix : mfixpoint term) (idx : nat) (args : list term) (narg : nat) (fn : term)
            (Hufix : unfold_fix mfix idx = Some (narg, fn))
            (Hisctor : is_constructor narg args = true),
        P cf Σ Γ pb (mkApps (tFix mfix idx) args) (mkApps fn args)
          (cumul_fix _ _ _ _ _ _ _ _ Hufix Hisctor)) →

    (* cofix unfolding *)
    (∀ (Γ : context) (pb : conv_pb) ci (p : predicate term) (mfix : mfixpoint term) (idx : nat)
            (args : list term) (narg : nat) (fn : term) (brs : list (branch term))
            (Hucofix : unfold_cofix mfix idx = Some (narg, fn)),
        P cf Σ Γ pb (tCase ci p (mkApps (tCoFix mfix idx) args) brs) (tCase ci p (mkApps fn args) brs)
          (cumul_cofix_case _ _ _ _ _ _ _ _ _ _ _ Hucofix)) →

    (∀ (Γ : context) (pb : conv_pb) (p : projection) (mfix : mfixpoint term) (idx : nat) (args : list term)
            (narg : nat) (fn : term)
            (Hucofix : unfold_cofix mfix idx = Some (narg, fn)),
        P cf Σ Γ pb (tProj p (mkApps (tCoFix mfix idx) args)) (tProj p (mkApps fn args))
          (cumul_cofix_proj _ _ _ _ _ _ _ _ _ Hucofix)) →

    (* constant unfolding *)
    (∀ (Γ : context) (pb : conv_pb) c (decl : constant_body) (body : term)
            (Hdecl_decl : declared_constant Σ c decl)
            (u : Instance.t)
            (Hdecl_body : cst_body decl = Some body),
        P cf Σ Γ pb (tConst c u) (subst_instance u body)
          (cumul_delta _ _ _ _ _ _ Hdecl_decl _ Hdecl_body)) →

    (* Proj *)
    (∀ (Γ : context) (pb : conv_pb)p (args : list term) (u : Instance.t)
            (arg : term)
            (Hargs : nth_error args (p.(proj_npars) + p.(proj_arg)) = Some arg),
        P cf Σ Γ pb (tProj p (mkApps (tConstruct p.(proj_ind) 0 u) args)) arg
          (cumul_proj _ _ _ _ _ _ _ Hargs)) →

    (* transitivity *)
    (∀ (Γ : context) (pb : conv_pb) (t u v : term)
            (Hclosed_ctx : is_closed_context Γ) (Hopen_term : is_open_term Γ u)
            (Htu : cumulSpec0 Σ Γ pb t u) (_ : P cf Σ Γ pb t u Htu)
            (Huv : cumulSpec0 Σ Γ pb u v) (_ : P cf Σ Γ pb u v Huv),
        P cf Σ Γ pb t v
          (cumul_Trans _ _ _ _ _ _ Hclosed_ctx Hopen_term Htu Huv)) →

    (* symmetry *)
    (∀ (Γ : context) (pb : conv_pb) (t u : term)
            (Hut : cumulSpec0 Σ Γ Conv u t) (_ : P cf Σ Γ Conv u t Hut),
        P cf Σ Γ pb t u
          (cumul_Sym _ _ _ _ _ Hut)) →

    (* reflexivity *)
    (∀ (Γ : context) (pb : conv_pb) (t : term),
        P cf Σ Γ pb t t
          (cumul_Refl _ _ _ _)) →

    (* congruence rules *)

    (∀ (Γ : context) (pb : conv_pb) (ev : nat) (l l' : list term)
            (H : All2 (cumulSpec0 Σ Γ Conv) l l') (_ : All2_dep (P cf Σ Γ Conv) H),
        P cf Σ Γ pb (tEvar ev l) (tEvar ev l')
          (cumul_Evar _ _ _ _ _ _ H)) →

    (∀ (Γ : context) (pb : conv_pb) (t t' u u' : term)
            (Htt' : cumulSpec0 Σ Γ pb t t') (_ : P cf Σ Γ pb t t' Htt')
            (Huu' : cumulSpec0 Σ Γ Conv u u') (_ : P cf Σ Γ Conv u u' Huu'),
        P cf Σ Γ pb (tApp t u) (tApp t' u')
          (cumul_App _ _ _ _ _ _ _ Htt' Huu')) →

    (∀ (Γ : context) (pb : conv_pb) (na na' : aname) (ty ty' t t' : term)
            (Hna : eq_binder_annot na na')
            (Hty : cumulSpec0 Σ Γ Conv ty ty') (_ : P cf Σ Γ Conv ty ty' Hty)
            (Ht : cumulSpec0 Σ (Γ ,, vass na ty) pb t t') ( _ : P cf Σ (Γ ,, vass na ty) pb t t' Ht),
        P cf Σ Γ pb (tLambda na ty t) (tLambda na' ty' t')
          (cumul_Lambda _ _ _ _ _ _ _ _ _ Hna Hty Ht)) →

    (∀ (Γ : context) (pb : conv_pb) (na na' : binder_annot name) (a a' b b' : term)
            (Hna : eq_binder_annot na na')
            (Ha : cumulSpec0 Σ Γ Conv a a') (_ : P cf Σ Γ Conv a a' Ha)
            (Hb : cumulSpec0 Σ (Γ,, vass na a) pb b b') (_ : P cf Σ (Γ,, vass na a) pb b b' Hb),
        P cf Σ Γ pb (tProd na a b) (tProd na' a' b')
          (cumul_Prod _ _ _ _ _ _ _ _ _ Hna Ha Hb)) →

    (∀ (Γ : context) (pb : conv_pb) (na na' : binder_annot name) (t t' ty ty' u u' : term)
            (Hna : eq_binder_annot na na')
            (Ht : cumulSpec0 Σ Γ Conv t t') (_ : P cf Σ Γ Conv t t' Ht)
            (Hty : cumulSpec0 Σ Γ Conv ty ty') (_ : P cf Σ Γ Conv ty ty' Hty)
            (Hu : cumulSpec0 Σ (Γ,, vdef na t ty) pb u u') (_ : P cf Σ (Γ,, vdef na t ty) pb u u' Hu),
        P cf Σ Γ pb (tLetIn na t ty u) (tLetIn na' t' ty' u')
          (cumul_LetIn _ _ _ _ _ _ _ _ _ _ _ Hna Ht Hty Hu)) →

    (∀ (Γ : context) (pb : conv_pb) (indn : case_info) (p p' : predicate term)
            (c c' : term) (brs brs' : list (branch term))
            (Hp : cumul_predicate (fun Γ ⇒ cumulSpec0 Σ Γ Conv) Γ (compare_universe Conv Σ) p p')
            (_ : cumul_predicate_dep Hp (fun Γ ⇒ P cf Σ Γ Conv) (fun _ _ _ ⇒ True))
            (Hc : cumulSpec0 Σ Γ Conv c c') (_ : P cf Σ Γ Conv c c' Hc)
            (Hbody : All2
                       (fun br br' : branch term ⇒
                          eq_context_gen eq eq (bcontext br) (bcontext br') ×
                            cumulSpec0 Σ (Γ,,, inst_case_branch_context p br) Conv
                              (bbody br) (bbody br'))
                       brs brs')
            (_ : All2_dep
                   (fun br br' Hc ⇒ P cf Σ (Γ,,, inst_case_branch_context p br) Conv (bbody br) (bbody br') (snd Hc)) Hbody),
        P cf Σ Γ pb (tCase indn p c brs) (tCase indn p' c' brs')
          (cumul_Case _ _ _ _ _ _ _ _ _ _ Hp Hc Hbody)) →

    (∀ (Γ : context) (pb : conv_pb)
            (p : projection) (c c' : term)
            (Hc : cumulSpec0 Σ Γ Conv c c') (_ : P cf Σ Γ Conv c c' Hc),
        P cf Σ Γ pb (tProj p c) (tProj p c')
          (cumul_Proj _ _ _ _ _ _ Hc)) →

    (∀ (Γ : context) (pb : conv_pb)
            (mfix : mfixpoint term) (mfix' : list (def term)) (idx : nat)
            (H : All2
                   (fun x y : def term ⇒
                      (cumulSpec0 Σ Γ Conv (dtype x) (dtype y))
                      × ((cumulSpec0 Σ (Γ,,, fix_context mfix) Conv (dbody x) (dbody y))
                           × (rarg x = rarg y)
                           × eq_binder_annot (dname x) (dname y)))
                   mfix mfix')
            (_ : All2_dep
                   (fun x y H
                    ⇒ P cf Σ Γ Conv (dtype x) (dtype y) (fst H) × P cf Σ (Γ,,, fix_context mfix) Conv (dbody x) (dbody y) (fst (snd H)))
                   H),
        P cf Σ Γ pb (tFix mfix idx) (tFix mfix' idx)
          (cumul_Fix _ _ _ _ _ _ H)) →

    (∀ (Γ : context) (pb : conv_pb)
            (mfix : mfixpoint term) (mfix' : list (def term)) (idx : nat)
            (H : All2
                   (fun x y : def term ⇒
                      (cumulSpec0 Σ Γ Conv (dtype x) (dtype y))
                        × ((cumulSpec0 Σ (Γ,,, fix_context mfix) Conv (dbody x) (dbody y))
                             × (rarg x = rarg y)
                             × (eq_binder_annot (dname x) (dname y))))
                   mfix mfix')
            (_ : All2_dep
                   (fun x y H
                    ⇒ P cf Σ Γ Conv (dtype x) (dtype y) (fst H) × P cf Σ (Γ,,, fix_context mfix) Conv (dbody x) (dbody y) (fst (snd H)))
                   H),
        P cf Σ Γ pb (tCoFix mfix idx) (tCoFix mfix' idx)
          (cumul_CoFix _ _ _ _ _ _ H)) →

    (* cumulativity rules *)

    (∀ (Γ : context) (pb : conv_pb) (i : inductive) (u u' : list Level.t)
            (args args' : list term)
            (Hu : R_global_instance Σ (eq_universe Σ) (compare_universe pb Σ) (IndRef i) #|args| u u')
            (Hargs : All2 (cumulSpec0 Σ Γ Conv) args args')
            (_ : All2_dep (P cf Σ Γ Conv) Hargs),
        P cf Σ Γ pb (mkApps (tInd i u) args) (mkApps (tInd i u') args')
          (cumul_Ind _ _ _ _ _ _ _ _ Hu Hargs)) →

    (∀ (Γ : context) (pb : conv_pb) (i : inductive) (k : nat)
            (u u' : list Level.t) (args args' : list term)
            (Hu : R_global_instance Σ (eq_universe Σ) (compare_universe pb Σ) (ConstructRef i k) #|args| u u')
            (Hargs : All2 (cumulSpec0 Σ Γ Conv) args args')
            (_ : All2_dep (P cf Σ Γ Conv) Hargs),
        P cf Σ Γ pb (mkApps (tConstruct i k u) args) (mkApps (tConstruct i k u') args')
          (cumul_Construct _ _ _ _ _ _ _ _ _ Hu Hargs)) →

    (∀ (Γ : context) (pb : conv_pb) (s s' : Universe.t)
            (Hs : compare_universe pb Σ s s'),
        P cf Σ Γ pb (tSort s) (tSort s')
          (cumul_Sort _ _ _ _ _ Hs)) →

    (∀ (Γ : context) (pb : conv_pb) (c : kername) (u u' : list Level.t)
            (Hu : R_universe_instance (compare_universe Conv Σ) u u'),
        P cf Σ Γ pb (tConst c u) (tConst c u')
          (cumul_Const _ _ _ _ _ _ Hu)) →

    ∀ (Γ : context) (pb : conv_pb) (t t0 : term) (Ht : @cumulSpec0 cf Σ Γ pb t t0), P cf Σ Γ pb t t0 Ht.
Proof.
  intros. rename Ht into Xlast.
  revert Γ pb t t0 Xlast.
  fix aux 5. intros Γ pb t u Xlast.
  move aux at top.
  destruct Xlast.
  - eapply X8; eauto.
  - eapply X9; eauto.
  - eapply X10; eauto.
  - eapply X20; eauto. clear -a aux.
    revert args args' a.
    fix aux' 3; destruct a; constructor; auto.
  - eapply X21; eauto. clear -a aux.
    revert args args' a.
    fix aux' 3; destruct a; constructor; auto.
  - eapply X22; eauto.
  - eapply X23; eauto.
  - eapply X11; eauto.
    revert args args' a.
    fix aux' 3; destruct a; constructor; auto.
  - eapply X12; eauto.
  - eapply X13; eauto.
  - eapply X14; eauto.
  - eapply X15; eauto.
  - eapply X16 ; eauto.
    + unfold cumul_predicate in ×. destruct c0 as [c0 [cuniv [ccontext creturn]]].
      repeat split ; eauto.
      × revert c0. generalize (pparams p), (pparams p').
        fix aux' 3; destruct c0; constructor; auto.
      × apply Forall2_dep_from_nth_error; intros; exact I.
    + revert brs brs' a.
      fix aux' 3; destruct a; constructor; intuition auto.
  - eapply X17 ; eauto.
  - eapply X18 ; eauto.
    revert a.
    set (mfixAbs_context := fix_context mfix).
    clearbody mfixAbs_context.
    revert mfix mfix'.
    fix aux' 3; destruct a; constructor.
    + intuition auto.
    + auto.
  - eapply X19 ; eauto.
    revert a.
    set (mfixAbs_context := fix_context mfix).
    clearbody mfixAbs_context.
    revert mfix mfix'.
    fix aux' 3; destruct a; constructor.
    + intuition auto.
    + auto.
  - eapply X; eauto.
  - eapply X0; eauto.
  - eapply X1; eauto.
  - eapply X2; eauto.
  - eapply X3; eauto.
  - eapply X4; eauto.
  - eapply X5; eauto.
  - eapply X6; eauto.
  - eapply X7; eauto.
Defined.

Notation cumulSpec0_ind_all := cumulSpec0_rect (only parsing).

Definition cumulSpec0_rec
  : ∀ cf (Σ : global_env_ext)
           (P : ∀ cf Σ Γ pb u v, @cumulSpec0 cf Σ Γ pb u v → Set),
    _
  := cumulSpec0_rect.

Definition cumulSpec0_ind
  : ∀ cf (Σ : global_env_ext)
           (P : ∀ cf Σ Γ pb u v, @cumulSpec0 cf Σ Γ pb u v → Prop),
    _
  := cumulSpec0_rec.

Lemma convSpec0_ind_all :
  ∀ cf (Σ : global_env_ext)
         (P : ∀ cf Σ Γ pb u v, @cumulSpec0 cf Σ Γ pb u v → Type),

        (* beta *)
       (∀ (Γ : context) (na : aname) (t b a : term),
        P cf Σ Γ Conv (tApp (tLambda na t b) a) (b {0 := a}) (cumul_beta _ _ _ _ _ _ _)) →

        (* let *)
       (∀ (Γ : context) (na : aname) (b t b' : term), P cf Σ Γ Conv (tLetIn na b t b') (b' {0 := b}) (cumul_zeta _ _ _ _ _ _ _)) →

       (∀ (Γ : context) (i : nat) (body : term)
               (pf : option_map decl_body (nth_error Γ i) = Some (Some body)),
           P cf Σ Γ Conv (tRel i) ((lift0 (S i)) body) (cumul_rel _ _ _ _ _ pf)) →

        (* iota *)
       (∀ (Γ : context) (ci : case_info) (c : nat) (u : Instance.t) (args : list term)
          (p : predicate term) (brs : list (branch term)) br
          (Hbrs : nth_error brs c = Some br)
          (Hnargs : #|args| = (ci.(ci_npar) + context_assumptions br.(bcontext))%nat),
           P cf Σ Γ Conv (tCase ci p (mkApps (tConstruct ci.(ci_ind) c u) args) brs)
             (iota_red ci.(ci_npar) p args br)
             (cumul_iota _ _ _ _ _ _ _ _ _ _ Hbrs Hnargs)) →

        (* fix unfolding *)
       (∀ (Γ : context) (mfix : mfixpoint term) (idx : nat) (args : list term) (narg : nat) (fn : term)
               (Hufix : unfold_fix mfix idx = Some (narg, fn))
               (Hisctor : is_constructor narg args = true),
           P cf Σ Γ Conv (mkApps (tFix mfix idx) args) (mkApps fn args)
             (cumul_fix _ _ _ _ _ _ _ _ Hufix Hisctor)) →

      (* cofix unfolding *)
       (∀ (Γ : context) ci (p : predicate term) (mfix : mfixpoint term) (idx : nat)
               (args : list term) (narg : nat) (fn : term) (brs : list (branch term))
               (Hucofix : unfold_cofix mfix idx = Some (narg, fn)),
           P cf Σ Γ Conv (tCase ci p (mkApps (tCoFix mfix idx) args) brs) (tCase ci p (mkApps fn args) brs)
             (cumul_cofix_case _ _ _ _ _ _ _ _ _ _ _ Hucofix)) →

       (∀ (Γ : context) (p : projection) (mfix : mfixpoint term) (idx : nat) (args : list term)
               (narg : nat) (fn : term)
               (Hucofix : unfold_cofix mfix idx = Some (narg, fn)),
           P cf Σ Γ Conv (tProj p (mkApps (tCoFix mfix idx) args)) (tProj p (mkApps fn args))
             (cumul_cofix_proj _ _ _ _ _ _ _ _ _ Hucofix)) →

        (* constant unfolding *)
       (∀ (Γ : context) c (decl : constant_body) (body : term)
               (Hdecl_decl : declared_constant Σ c decl)
               (u : Instance.t)
               (Hdecl_body : cst_body decl = Some body),
           P cf Σ Γ Conv (tConst c u) (subst_instance u body)
             (cumul_delta _ _ _ _ _ _ Hdecl_decl _ Hdecl_body)) →

        (* Proj *)
       (∀ (Γ : context)p (args : list term) (u : Instance.t)
               (arg : term)
               (Hargs : nth_error args (p.(proj_npars) + p.(proj_arg)) = Some arg),
           P cf Σ Γ Conv (tProj p (mkApps (tConstruct p.(proj_ind) 0 u) args)) arg
             (cumul_proj _ _ _ _ _ _ _ Hargs)) →

        (* transitivity *)
       (∀ (Γ : context) (t u v : term)
               (Hclosed_ctx : is_closed_context Γ) (Hopen_term : is_open_term Γ u)
               (Htu : cumulSpec0 Σ Γ Conv t u) (_ : P cf Σ Γ Conv t u Htu)
               (Huv : cumulSpec0 Σ Γ Conv u v) (_ : P cf Σ Γ Conv u v Huv),
           P cf Σ Γ Conv t v
             (cumul_Trans _ _ _ _ _ _ Hclosed_ctx Hopen_term Htu Huv)) →

        (* symmetry *)
       (∀ (Γ : context) (t u : term)
               (Hut : cumulSpec0 Σ Γ Conv u t) (_ : P cf Σ Γ Conv u t Hut),
           P cf Σ Γ Conv t u
             (cumul_Sym _ _ _ _ _ Hut)) →

        (* reflexivity *)
        (∀ (Γ : context) (t : term),
            P cf Σ Γ Conv t t
              (cumul_Refl _ _ _ _)) →

        (* congruence rules *)

        (∀ (Γ : context) (ev : nat) (l l' : list term)
                (H : All2 (cumulSpec0 Σ Γ Conv) l l') (_ : All2_dep (P cf Σ Γ Conv) H),
            P cf Σ Γ Conv (tEvar ev l) (tEvar ev l')
              (cumul_Evar _ _ _ _ _ _ H)) →

        (∀ (Γ : context) (t t' u u' : term)
                (Htt' : cumulSpec0 Σ Γ Conv t t') (_ : P cf Σ Γ Conv t t' Htt')
                (Huu' : cumulSpec0 Σ Γ Conv u u') (_ : P cf Σ Γ Conv u u' Huu'),
            P cf Σ Γ Conv (tApp t u) (tApp t' u')
              (cumul_App _ _ _ _ _ _ _ Htt' Huu')) →

        (∀ (Γ : context) (na na' : aname) (ty ty' t t' : term)
                (Hna : eq_binder_annot na na')
                (Hty : cumulSpec0 Σ Γ Conv ty ty') (_ : P cf Σ Γ Conv ty ty' Hty)
                (Ht : cumulSpec0 Σ (Γ ,, vass na ty) Conv t t') ( _ : P cf Σ (Γ ,, vass na ty) Conv t t' Ht),
            P cf Σ Γ Conv (tLambda na ty t) (tLambda na' ty' t')
              (cumul_Lambda _ _ _ _ _ _ _ _ _ Hna Hty Ht)) →

        (∀ (Γ : context) (na na' : binder_annot name) (a a' b b' : term)
                (Hna : eq_binder_annot na na')
                (Ha : cumulSpec0 Σ Γ Conv a a') (_ : P cf Σ Γ Conv a a' Ha)
                (Hb : cumulSpec0 Σ (Γ,, vass na a) Conv b b') (_ : P cf Σ (Γ,, vass na a) Conv b b' Hb),
            P cf Σ Γ Conv (tProd na a b) (tProd na' a' b')
              (cumul_Prod _ _ _ _ _ _ _ _ _ Hna Ha Hb)) →

     (∀ (Γ : context) (na na' : binder_annot name) (t t' ty ty' u u' : term)
             (Hna : eq_binder_annot na na')
             (Ht : cumulSpec0 Σ Γ Conv t t') (_ : P cf Σ Γ Conv t t' Ht)
             (Hty : cumulSpec0 Σ Γ Conv ty ty') (_ : P cf Σ Γ Conv ty ty' Hty)
             (Hu : cumulSpec0 Σ (Γ,, vdef na t ty) Conv u u') (_ : P cf Σ (Γ,, vdef na t ty) Conv u u' Hu),
         P cf Σ Γ Conv (tLetIn na t ty u) (tLetIn na' t' ty' u')
           (cumul_LetIn _ _ _ _ _ _ _ _ _ _ _ Hna Ht Hty Hu)) →

      (∀ (Γ : context) (indn : case_info) (p p' : predicate term)
              (c c' : term) (brs brs' : list (branch term))
              (Hp : cumul_predicate (fun Γ ⇒ cumulSpec0 Σ Γ Conv) Γ (compare_universe Conv Σ) p p')
              (_ : cumul_predicate_dep Hp (fun Γ ⇒ P cf Σ Γ Conv) (fun _ _ _ ⇒ True))
              (Hc : cumulSpec0 Σ Γ Conv c c') (_ : P cf Σ Γ Conv c c' Hc)
              (Hbody : All2
                         (fun br br' : branch term ⇒
                            eq_context_gen eq eq (bcontext br) (bcontext br') ×
                              cumulSpec0 Σ (Γ,,, inst_case_branch_context p br) Conv
                                (bbody br) (bbody br'))
                         brs brs')
              (_ : All2_dep
                     (fun br br' Hc ⇒ P cf Σ (Γ,,, inst_case_branch_context p br) Conv (bbody br) (bbody br') (snd Hc)) Hbody),
          P cf Σ Γ Conv (tCase indn p c brs) (tCase indn p' c' brs')
            (cumul_Case _ _ _ _ _ _ _ _ _ _ Hp Hc Hbody)) →

       (∀ (Γ : context)
               (p : projection) (c c' : term)
               (Hc : cumulSpec0 Σ Γ Conv c c') (_ : P cf Σ Γ Conv c c' Hc),
           P cf Σ Γ Conv (tProj p c) (tProj p c')
             (cumul_Proj _ _ _ _ _ _ Hc)) →

       (∀ (Γ : context)
               (mfix : mfixpoint term) (mfix' : list (def term)) (idx : nat)
               (H : All2
            (fun x y : def term ⇒
               (cumulSpec0 Σ Γ Conv (dtype x) (dtype y))
               × ((cumulSpec0 Σ (Γ,,, fix_context mfix) Conv (dbody x) (dbody y))
                    × (rarg x = rarg y)
                    × eq_binder_annot (dname x) (dname y)))
            mfix mfix')
               (_ : All2_dep
                      (fun x y H
                       ⇒ P cf Σ Γ Conv (dtype x) (dtype y) (fst H) × P cf Σ (Γ,,, fix_context mfix) Conv (dbody x) (dbody y) (fst (snd H)))
                      H),
           P cf Σ Γ Conv (tFix mfix idx) (tFix mfix' idx)
             (cumul_Fix _ _ _ _ _ _ H)) →

       (∀ (Γ : context)
               (mfix : mfixpoint term) (mfix' : list (def term)) (idx : nat)
               (H : All2
             (fun x y : def term ⇒
                (cumulSpec0 Σ Γ Conv (dtype x) (dtype y))
                  × ((cumulSpec0 Σ (Γ,,, fix_context mfix) Conv (dbody x) (dbody y))
                       × (rarg x = rarg y)
                       × (eq_binder_annot (dname x) (dname y))))
             mfix mfix')
               (_ : All2_dep
                      (fun x y H
                       ⇒ P cf Σ Γ Conv (dtype x) (dtype y) (fst H) × P cf Σ (Γ,,, fix_context mfix) Conv (dbody x) (dbody y) (fst (snd H)))
                      H),
           P cf Σ Γ Conv (tCoFix mfix idx) (tCoFix mfix' idx)
             (cumul_CoFix _ _ _ _ _ _ H)) →

      (* cumulativity rules *)

      (∀ (Γ : context) (i : inductive) (u u' : list Level.t)
              (args args' : list term)
              (Hu : R_global_instance Σ (eq_universe Σ) (compare_universe Conv Σ) (IndRef i) #|args| u u')
              (Hargs : All2 (cumulSpec0 Σ Γ Conv) args args')
              (_ : All2_dep (P cf Σ Γ Conv) Hargs),
          P cf Σ Γ Conv (mkApps (tInd i u) args) (mkApps (tInd i u') args')
            (cumul_Ind _ _ _ _ _ _ _ _ Hu Hargs)) →

    (∀ (Γ : context) (i : inductive) (k : nat)
            (u u' : list Level.t) (args args' : list term)
            (Hu : R_global_instance Σ (eq_universe Σ) (compare_universe Conv Σ) (ConstructRef i k) #|args| u u')
            (Hargs : All2 (cumulSpec0 Σ Γ Conv) args args')
            (_ : All2_dep (P cf Σ Γ Conv) Hargs),
        P cf Σ Γ Conv (mkApps (tConstruct i k u) args) (mkApps (tConstruct i k u') args')
          (cumul_Construct _ _ _ _ _ _ _ _ _ Hu Hargs)) →

      (∀ (Γ : context) (s s' : Universe.t)
              (Hs : compare_universe Conv Σ s s'),
          P cf Σ Γ Conv (tSort s) (tSort s')
            (cumul_Sort _ _ _ _ _ Hs)) →

      (∀ (Γ : context) (c : kername) (u u' : list Level.t)
              (Hu : R_universe_instance (compare_universe Conv Σ) u u'),
          P cf Σ Γ Conv (tConst c u) (tConst c u')
            (cumul_Const _ _ _ _ _ _ Hu)) →

       ∀ (Γ : context) (t t0 : term) (Ht : cumulSpec0 Σ Γ Conv t t0), P cf Σ Γ Conv t t0 Ht.
Proof.
  intros.
  remember Conv as pb eqn:Hpb in Ht |- ×.
  induction Ht; eauto; subst.
  all: exactly_once (idtac; multimatch goal with H : _ |- _ ⇒ eapply H end; eauto).
  all: cbv [cumul_predicate_dep] in ×.
  all: repeat destruct ?; subst.
  all: destruct_head'_prod.
  all: repeat split; eauto.
  all: eapply All2_dep_impl; tea; cbv beta; intuition auto.
Defined.