Library MetaCoq.PCUIC.PCUICInductiveInversion

From Coq Require Import Utf8.
From MetaCoq.Template Require Import config utils.
From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICTactics PCUICInduction
     PCUICLiftSubst PCUICUnivSubst
     PCUICTyping PCUICGlobalEnv
     PCUICWeakeningEnv PCUICWeakeningEnvTyp
     PCUICWeakeningConv PCUICWeakeningTyp
     PCUICSigmaCalculus
     PCUICSubstitution PCUICClosed PCUICClosedConv PCUICClosedTyp
     PCUICCumulativity PCUICGeneration PCUICReduction
     PCUICEquality PCUICConfluence PCUICCasesContexts
     PCUICOnFreeVars PCUICContextConversion PCUICContextConversionTyp PCUICContextSubst
     PCUICUnivSubstitutionConv PCUICUnivSubstitutionTyp
     PCUICConversion PCUICInversion PCUICContexts PCUICArities
     PCUICSpine PCUICInductives PCUICWellScopedCumulativity PCUICValidity.

Require Import Equations.Type.Relation_Properties.
Require Import Equations.Prop.DepElim.
From Equations Require Import Equations.
Derive Subterm for term.
Require Import ssreflect.

Local Set SimplIsCbn.

Implicit Types (cf : checker_flags) (Σ : global_env_ext).

#[global]
Hint Rewrite reln_length : len.

#[global] Hint Resolve f_equal_nat : arith.

Ltac substu := autorewrite with substu ⇒ /=.

Tactic Notation "substu" "in" hyp(id) :=
  autorewrite with substu in id; simpl in id.

Lemma conv_eq_ctx {cf:checker_flags} Σ Γ Γ' T U : Σ ;;; Γ |- T = U → Γ = Γ' → Σ ;;; Γ' |- T = U.
Proof. now intros H →. Qed.

Ltac pcuic := intuition eauto 5 with pcuic ||
  (try solve [repeat red; cbn in *; intuition auto; eauto 5 with pcuic || (try lia || congruence)]).

Lemma declared_constructor_valid_ty {cf:checker_flags} Σ Γ mdecl idecl i n cdecl u :
  wf Σ.1 →
  wf_local Σ Γ →
  declared_constructor Σ.1 (i, n) mdecl idecl cdecl →
  consistent_instance_ext Σ (ind_universes mdecl) u →
  isType Σ Γ (type_of_constructor mdecl cdecl (i, n) u).
Proof.
  move⇒ wfΣ wfΓ declc Hu.
  eapply validity. eapply type_Construct; eauto.
Qed.

Lemma type_tFix_inv {cf:checker_flags} (Σ : global_env_ext) Γ mfix idx T : wf Σ →
  Σ ;;; Γ |- tFix mfix idx : T →
  { T' & { rarg & {f & (unfold_fix mfix idx = Some (rarg, f)) ×
    wf_fixpoint Σ mfix
  × (Σ ;;; Γ |- f : T') × (Σ ;;; Γ ⊢ T' ≤ T) }}}%type.
Proof.
  intros wfΣ H. depind H.
  - unfold unfold_fix. rewrite e.
    specialize (nth_error_all e a0) as [s Hs].
    specialize (nth_error_all e a1) as Hty.
    simpl.
    destruct decl as [name ty body rarg]; simpl in ×.
    clear e.
    eexists _, _, _. split.
    + split.
      × eauto.
      × eapply (substitution (Δ := [])); simpl; eauto with wf.
        rename i into hguard. clear -f a a0 a1 hguard.
        pose proof a1 as a1'. apply All_rev in a1'.
        unfold fix_subst, fix_context. simpl.
        revert a1'. rewrite <- (@List.rev_length _ mfix).
        rewrite rev_mapi. unfold mapi.
        assert (#|mfix| ≥ #|List.rev mfix|) by (rewrite List.rev_length; lia).
        assert (He :0 = #|mfix| - #|List.rev mfix|) by (rewrite List.rev_length; auto with arith).
        rewrite {3}He. clear He. revert H.
        assert (∀ i, i < #|List.rev mfix| → nth_error (List.rev mfix) i = nth_error mfix (#|List.rev mfix| - S i)).
        { intros. rewrite nth_error_rev. 1: auto.
          now rewrite List.rev_length List.rev_involutive. }
        revert H.
        generalize (List.rev mfix).
        intros l Hi Hlen H.
        induction H.
        ++ simpl. constructor.
        ++ simpl. constructor.
          ** unfold mapi in IHAll.
              simpl in Hlen. replace (S (#|mfix| - S #|l|)) with (#|mfix| - #|l|) by lia.
              apply IHAll.
              --- intros. simpl in Hi. specialize (Hi (S i)). apply Hi. lia.
              --- lia.
          ** clear IHAll.
              simpl in Hlen. assert ((Nat.pred #|mfix| - (#|mfix| - S #|l|)) = #|l|) by lia.
              rewrite H0. rewrite simpl_subst_k.
              --- clear. induction l; simpl; auto with arith.
              --- eapply type_Fix; auto.
                  simpl in Hi. specialize (Hi 0). forward Hi.
                  +++ lia.
                  +++ simpl in Hi.
                      rewrite Hi. f_equal. lia.

    + rewrite simpl_subst_k.
      × now rewrite fix_context_length fix_subst_length.
      × eapply isType_ws_cumul_pb_refl; pcuic.
  - destruct (IHtyping1 wfΣ) as [T' [rarg [f [[unf fty] Hcumul]]]].
    ∃ T', rarg, f. intuition auto.
    etransitivity; eauto.
    eapply PCUICConversion.cumulSpec_cumulAlgo_curry in c; eauto; fvs.
Qed.

Lemma subslet_cofix {cf:checker_flags} (Σ : global_env_ext) Γ mfix :
  wf_local Σ Γ →
  cofix_guard Σ Γ mfix →
  All (fun d : def term ⇒ ∑ s : Universe.t, Σ;;; Γ |- dtype d : tSort s) mfix →
  All
  (fun d : def term ⇒
   Σ;;; Γ ,,, fix_context mfix |- dbody d
   : lift0 #|fix_context mfix| (dtype d)) mfix →
  wf_cofixpoint Σ mfix → subslet Σ Γ (cofix_subst mfix) (fix_context mfix).
Proof.
  intros wfΓ hguard types bodies wfcofix.
  pose proof bodies as X1. apply All_rev in X1.
  unfold cofix_subst, fix_context. simpl.
  revert X1. rewrite <- (@List.rev_length _ mfix).
  rewrite rev_mapi. unfold mapi.
  assert (#|mfix| ≥ #|List.rev mfix|) by (rewrite List.rev_length; lia).
  assert (He :0 = #|mfix| - #|List.rev mfix|) by (rewrite List.rev_length; auto with arith).
  rewrite {3}He. clear He. revert H.
  assert (∀ i, i < #|List.rev mfix| → nth_error (List.rev mfix) i = nth_error mfix (#|List.rev mfix| - S i)).
  { intros. rewrite nth_error_rev. 1: auto.
    now rewrite List.rev_length List.rev_involutive. }
  revert H.
  generalize (List.rev mfix).
  intros l Hi Hlen H.
  induction H.
  ++ simpl. constructor.
  ++ simpl. constructor.
    ** unfold mapi in IHAll.
        simpl in Hlen. replace (S (#|mfix| - S #|l|)) with (#|mfix| - #|l|) by lia.
        apply IHAll.
        --- intros. simpl in Hi. specialize (Hi (S i)). apply Hi. lia.
        --- lia.
    ** clear IHAll.
        simpl in Hlen. assert ((Nat.pred #|mfix| - (#|mfix| - S #|l|)) = #|l|) by lia.
        rewrite H0. rewrite simpl_subst_k.
        --- clear. induction l; simpl; auto with arith.
        --- eapply type_CoFix; auto.
            simpl in Hi. specialize (Hi 0). forward Hi.
            +++ lia.
            +++ simpl in Hi.
                rewrite Hi. f_equal. lia.
Qed.

Lemma type_tCoFix_inv {cf:checker_flags} (Σ : global_env_ext) Γ mfix idx T : wf Σ →
  Σ ;;; Γ |- tCoFix mfix idx : T →
  ∑ d, (nth_error mfix idx = Some d) ×
    wf_cofixpoint Σ mfix ×
    (Σ ;;; Γ |- subst0 (cofix_subst mfix) (dbody d) : (dtype d)) ×
    (Σ ;;; Γ ⊢ dtype d ≤ T).
Proof.
  intros wfΣ H. depind H.
  - ∃ decl.
    specialize (nth_error_all e a1) as Hty.
    destruct decl as [name ty body rarg]; simpl in ×.
    intuition auto.
    × eapply (substitution (s := cofix_subst mfix) (Δ := [])) in Hty. simpl; eauto with wf.
      simpl in Hty.
      rewrite subst_context_nil /= in Hty.
      eapply refine_type; eauto.
      rewrite simpl_subst_k //. len.
      apply subslet_cofix; auto.
    × eapply nth_error_all in a0; tea. cbn in a0. now eapply isType_ws_cumul_pb_refl.
  - destruct (IHtyping1 wfΣ) as [d [[[Hnth wfcofix] ?] ?]].
    ∃ d. intuition auto.
    etransitivity; eauto.
    now eapply PCUICConversion.cumulSpec_cumulAlgo_curry in c; tea; fvs.
Qed.

Lemma wf_cofixpoint_all {cf:checker_flags} (Σ : global_env_ext) mfix :
  wf_cofixpoint Σ mfix →
  ∑ mind, check_recursivity_kind (lookup_env Σ) mind CoFinite ×
  All (fun d ⇒ ∑ ctx i u args, (dtype d) = it_mkProd_or_LetIn ctx (mkApps (tInd {| inductive_mind := mind; inductive_ind := i |} u) args)) mfix.
Proof.
  unfold wf_cofixpoint, wf_cofixpoint_gen.
  destruct mfix. discriminate.
  simpl.
  destruct (check_one_cofix d) as [ind|] eqn:hcof.
  intros eqr.
  ∃ ind.
  destruct (map_option_out (map check_one_cofix mfix)) eqn:eqfixes.
  move/andb_and: eqr ⇒ [eqinds rk].
  split; auto.
  constructor.
  - move: hcof. unfold check_one_cofix.
    destruct d as [dname dbody dtype rarg] ⇒ /=.
    destruct (decompose_prod_assum [] dbody) as [ctx concl] eqn:Hdecomp.
    apply decompose_prod_assum_it_mkProd_or_LetIn in Hdecomp.
    destruct (decompose_app concl) eqn:dapp.
    destruct (destInd t) as [[ind' u]|] eqn:dind.
    destruct ind' as [mind ind'].
    move⇒ [=] Hmind. subst mind.
    ∃ ctx, ind', u, l0.
    simpl in Hdecomp. rewrite Hdecomp.
    f_equal.
    destruct t; try discriminate.
    simpl in dind. noconf dind.
    apply decompose_app_inv in dapp ⇒ //.
    discriminate.
  - clear rk hcof.
    induction mfix in l, eqfixes, eqinds |- ×. constructor.
    simpl in ×.
    destruct (check_one_cofix a) eqn:hcof; try discriminate.
    destruct (map_option_out (map check_one_cofix mfix)) eqn:hcofs; try discriminate.
    noconf eqfixes.
    specialize (IHmfix _ eq_refl).
    simpl in eqinds.
    move/andb_and: eqinds ⇒ [eqk eql0].
    constructor; auto. clear IHmfix hcofs d.
    destruct a as [dname dbody dtype rarg] ⇒ /=.
    unfold check_one_cofix in hcof.
    destruct (decompose_prod_assum [] dbody) as [ctx concl] eqn:Hdecomp.
    apply decompose_prod_assum_it_mkProd_or_LetIn in Hdecomp.
    destruct (decompose_app concl) eqn:dapp.
    destruct (destInd t) as [[ind' u]|] eqn:dind.
    destruct ind' as [mind ind']. noconf hcof.
    ∃ ctx, ind', u, l.
    simpl in Hdecomp. rewrite Hdecomp.
    f_equal.
    destruct t; try discriminate.
    simpl in dind. noconf dind.
    apply decompose_app_inv in dapp ⇒ //.
    rewrite dapp. do 3 f_equal.
    symmetry.
    change (eq_kername ind k) with (ReflectEq.eqb ind k) in eqk.
    destruct (ReflectEq.eqb_spec ind k); auto.
    discriminate.
  - discriminate.
  - discriminate.
Qed.

Section OnConstructor.
  Context {cf:checker_flags} {Σ : global_env} {ind mdecl idecl cdecl}
    {wfΣ: wf Σ} (declc : declared_constructor Σ ind mdecl idecl cdecl).

  Lemma on_constructor_wf_args :
    wf_local (Σ, ind_universes mdecl)
    (arities_context (ind_bodies mdecl) ,,, ind_params mdecl ,,, cstr_args cdecl).
  Proof using declc wfΣ.
    pose proof (on_declared_constructor declc) as [[onmind oib] [cunivs [hnth onc]]].
    pose proof (on_cargs onc). simpl in X.
    eapply sorts_local_ctx_wf_local in X ⇒ //. clear X.
    eapply weaken_wf_local ⇒ //.
    eapply wf_arities_context; eauto. eapply declc.
    now eapply onParams.
  Qed.

  Lemma on_constructor_subst :
    wf_global_ext Σ (ind_universes mdecl) ×
    wf_local (Σ, ind_universes mdecl)
    (arities_context (ind_bodies mdecl) ,,, ind_params mdecl ,,, cstr_args cdecl) ×
    ∑ inst,
    spine_subst (Σ, ind_universes mdecl)
              (arities_context (ind_bodies mdecl) ,,, ind_params mdecl ,,,
                cstr_args cdecl)
              ((to_extended_list_k (ind_params mdecl) #|cstr_args cdecl|) ++
                (cstr_indices cdecl)) inst
            (ind_params mdecl ,,, ind_indices idecl).
  Proof using declc wfΣ.
    pose proof (on_declared_constructor declc) as [[onmind oib] [cunivs [hnth onc]]].
    pose proof (onc.(on_cargs)). simpl in X.
    split. split. split.
    2:{ eapply (weaken_lookup_on_global_env' _ _ (InductiveDecl mdecl)); tea.
        eapply declc. }
    red. apply wfΣ.
    eapply sorts_local_ctx_wf_local in X ⇒ //. clear X.
    eapply weaken_wf_local ⇒ //.
    eapply wf_arities_context; eauto; eapply declc.
    now eapply onParams.
    destruct (on_ctype onc).
    rewrite onc.(cstr_eq) in t.
    rewrite -it_mkProd_or_LetIn_app in t.
    eapply inversion_it_mkProd_or_LetIn in t ⇒ //.
    unfold cstr_concl_head in t. simpl in t.
    eapply inversion_mkApps in t as [A [ta sp]].
    eapply inversion_Rel in ta as [decl [wfΓ [nth cum']]].
    rewrite nth_error_app_ge in nth. len.
    len in nth.
    all:auto.
    assert ((#|ind_bodies mdecl| - S (inductive_ind ind.1) + #|ind_params mdecl| +
    #|cstr_args cdecl| -
    (#|cstr_args cdecl| + #|ind_params mdecl|)) = #|ind_bodies mdecl| - S (inductive_ind ind.1)) by lia.
    move: nth; rewrite H; clear H.
    case: nth_error_spec ⇒ // /= decl' Hdecl Hlen.
    intros [= ->].
    eapply (nth_errror_arities_context (Σ := (Σ, ind_universes mdecl)) declc) in Hdecl; eauto.
    rewrite Hdecl in cum'; clear Hdecl.
    assert(closed (ind_type idecl)).
    { pose proof (oib.(onArity)). rewrite (oib.(ind_arity_eq)) in X0 |- ×.
      destruct X0 as [s Hs]. now apply subject_closed in Hs. }
    rewrite lift_closed in cum' ⇒ //.
    eapply typing_spine_strengthen in sp; simpl.
    3:tea.
    move: sp.
    rewrite (oib.(ind_arity_eq)).
    rewrite -it_mkProd_or_LetIn_app.
    move⇒ sp. simpl in sp.
    apply (arity_typing_spine (Σ := (Σ, ind_universes mdecl))) in sp as [Hlen' Hleq [inst Hinst]] ⇒ //.
    clear Hlen'.
    rewrite [_ ,,, _]app_context_assoc in Hinst.
    now ∃ inst.
    apply infer_typing_sort_impl with id oib.(onArity); intros Hs.
    now eapply weaken_ctx in Hs.
  Qed.
End OnConstructor.

Section OnConstructorExt.
  Context {cf} {Σ} {wfΣ : wf Σ} {ind mdecl idecl cdecl}
    (declc : declared_constructor Σ ind mdecl idecl cdecl).

  Lemma on_constructor_inst_wf_args u :
    consistent_instance_ext Σ (ind_universes mdecl) u →
    wf_local Σ ((ind_params mdecl)@[u] ,,, subst_context (ind_subst mdecl (fst ind) u) #|ind_params mdecl| (cstr_args cdecl)@[u]).
  Proof using declc wfΣ.
    intros cu.
    pose proof (on_constructor_wf_args declc).
    eapply wf_local_subst_instance in X; tea.
    rewrite -[X in X ,,, _]app_context_nil_l - !app_context_assoc app_context_assoc in X.
    rewrite !subst_instance_app_ctx /= in X.
    eapply substitution_wf_local in X.
    2:eapply (subslet_inds declc); tea.
    2:{ eapply (declared_inductive_wf_global_ext Σ.1 _ _ _ declc). }
    cbn in X. rewrite app_context_nil_l in X.
    rewrite subst_context_app Nat.add_0_r in X.
    rewrite closed_ctx_subst in X.
    rewrite closedn_subst_instance_context.
    eapply (declared_inductive_closed_params declc).
    now len in X.
  Qed.

  Lemma on_constructor_inst u :
    consistent_instance_ext Σ (ind_universes mdecl) u →
    wf_local Σ (subst_instance u
      (arities_context (ind_bodies mdecl) ,,, ind_params mdecl ,,, cstr_args cdecl)) ×
    ∑ inst,
    spine_subst Σ
            (subst_instance u
              (arities_context (ind_bodies mdecl) ,,, ind_params mdecl ,,,
                cstr_args cdecl))
            (map (subst_instance u)
              (to_extended_list_k (ind_params mdecl) #|cstr_args cdecl|) ++
            map (subst_instance u) (cstr_indices cdecl)) inst
            (subst_instance u (ind_params mdecl) ,,,
            subst_instance u (ind_indices idecl)).
  Proof using declc wfΣ.
    intros cu.
    destruct (on_constructor_subst declc) as [[wfext wfl] [inst sp]].
    eapply wf_local_subst_instance in wfl; eauto. split⇒ //.
    eapply spine_subst_inst in sp; eauto.
    rewrite map_app in sp. rewrite -subst_instance_app_ctx.
    eexists ; eauto.
  Qed.
End OnConstructorExt.

Lemma on_constructor_inst_pars_indices {cf:checker_flags} {Σ ind u mdecl idecl cdecl Γ pars parsubst} :
  wf Σ.1 →
  declared_constructor Σ.1 ind mdecl idecl cdecl →
  consistent_instance_ext Σ (ind_universes mdecl) u →
  spine_subst Σ Γ pars parsubst (subst_instance u (ind_params mdecl)) →
  wf_local Σ (subst_instance u (ind_params mdecl) ,,,
    subst_context (inds (inductive_mind ind.1) u (ind_bodies mdecl)) #|ind_params mdecl|
    (subst_instance u (cstr_args cdecl))) ×
  ∑ inst,
  spine_subst Σ
          (Γ ,,, subst_context parsubst 0 (subst_context (ind_subst mdecl ind.1 u) #|ind_params mdecl|
            (subst_instance u (cstr_args cdecl))))
          (map (subst parsubst #|cstr_args cdecl|)
            (map (subst (ind_subst mdecl ind.1 u) (#|cstr_args cdecl| + #|ind_params mdecl|))
              (map (subst_instance u) (cstr_indices cdecl))))
          inst
          (lift_context #|cstr_args cdecl| 0
          (subst_context parsubst 0 (subst_instance u (ind_indices idecl)))).
Proof.
  move⇒ wfΣ declc cext sp.
  destruct (on_constructor_inst declc u) as [wfl [inst sp']]; auto.
  rewrite !subst_instance_app in sp'.
  eapply spine_subst_app_inv in sp' as [spl spr]; auto.
  rewrite (spine_subst_extended_subst spl) in spr.
  rewrite subst_context_map_subst_expand_lets in spr; try now len.
  rewrite subst_instance_to_extended_list_k in spr.
  2:now len.
  rewrite lift_context_subst_context.
  rewrite app_assoc in spr.
  eapply spine_subst_subst_first in spr; eauto.
  2:eapply subslet_inds; eauto; eapply declc.
  len in spr.
  rewrite subst_context_app in spr.
  assert (closed_ctx (subst_instance u (ind_params mdecl)) ∧ closedn_ctx #|ind_params mdecl| (subst_instance u (ind_indices idecl)))
  as [clpars clinds].
  { pose proof (on_minductive_wf_params_indices declc).
    eapply closed_wf_local in X ⇒ //.
    rewrite closedn_ctx_app in X; simpl; eauto;
    move/andb_and: X; intuition auto;
    now rewrite closedn_subst_instance_context. }
  assert (closedn_ctx (#|ind_params mdecl| + #|cstr_args cdecl|) (subst_instance u (ind_indices idecl)))
    as clinds'.
  { eapply closedn_ctx_upwards; eauto. lia. }
  rewrite closed_ctx_subst // in spr.
  rewrite (closed_ctx_subst (inds (inductive_mind ind.1) u (ind_bodies mdecl)) _ (subst_context (List.rev _) _ _)) in spr.
  { len.
    rewrite -(Nat.add_0_r (#|cstr_args cdecl| + #|ind_params mdecl|)).
    eapply closedn_ctx_subst. len.
    rewrite -(context_assumptions_subst_instance u).
    eapply closedn_ctx_expand_lets. eapply closedn_ctx_upwards; eauto. lia.
    len. eapply closedn_ctx_upwards; eauto. lia.
    rewrite forallb_rev.
    rewrite PCUICLiftSubst.map_subst_instance_to_extended_list_k.
    eapply closedn_to_extended_list_k. }
  len in spr. split ⇒ //. apply spr.
  eapply spine_subst_weaken in spr.
  2:eapply (spine_dom_wf _ _ _ _ _ sp); eauto.
  rewrite app_context_assoc in spr.
  eapply spine_subst_subst in spr; eauto. 2:eapply sp.
  len in spr.
  rewrite {4}(spine_subst_extended_subst sp) in spr.
  rewrite subst_context_map_subst_expand_lets_k in spr; try now len.
  rewrite List.rev_length. now rewrite -(context_subst_length2 sp).
  rewrite expand_lets_k_ctx_subst_id' in spr. now len. now len.
  rewrite -subst_context_map_subst_expand_lets_k in spr; try len.
  rewrite subst_subst_context in spr. len in spr.
  rewrite subst_extended_lift // in spr.
  rewrite lift_extended_subst in spr.
  rewrite (map_map_compose _ _ _ _ (subst (List.rev pars) _)) in spr.
  assert (map
              (fun x : term ⇒
               subst (List.rev pars) #|cstr_args cdecl|
                 (lift0 #|cstr_args cdecl| x))
              (extended_subst (subst_instance u (ind_params mdecl)) 0) =
              (map
              (fun x : term ⇒
              (lift0 #|cstr_args cdecl|
                (subst (List.rev pars) 0 x)))
              (extended_subst (subst_instance u (ind_params mdecl)) 0))
              ).
  eapply map_ext ⇒ x.
  now rewrite -(commut_lift_subst_rec _ _ _ 0).
  rewrite H in spr. clear H.
  rewrite -(map_map_compose _ _ _ _ (lift0 #|cstr_args cdecl|)) in spr.
  rewrite -(spine_subst_extended_subst sp) in spr.
  rewrite subst_map_lift_lift_context in spr.
  rewrite -(context_subst_length sp).
  len.
  rewrite closed_ctx_subst //.
  rewrite (closed_ctx_subst (List.rev pars)) // in spr.
  eexists. eauto.
Qed.

Lemma mkApps_ind_typing_spine {cf:checker_flags} Σ Γ Γ' ind i
  inst ind' i' args args' :
  wf Σ.1 →
  wf_local Σ Γ →
  isType Σ Γ (it_mkProd_or_LetIn Γ' (mkApps (tInd ind i) args)) →
  typing_spine Σ Γ (it_mkProd_or_LetIn Γ' (mkApps (tInd ind i) args)) inst
    (mkApps (tInd ind' i') args') →
  ∑ instsubst,
  [× make_context_subst (List.rev Γ') inst [] = Some instsubst,
    #|inst| = context_assumptions Γ', ind = ind', R_ind_universes Σ ind #|args| i i',
    All2 (fun par par' ⇒ Σ ;;; Γ ⊢ par = par') (map (subst0 instsubst) args) args' &
    subslet Σ Γ instsubst Γ'].
Proof.
  intros wfΣ wfΓ; revert args args' ind i ind' i' inst.
  revert Γ'. refine (ctx_length_rev_ind _ _ _); simpl.
  - intros args args' ind i ind' i' inst wat Hsp.
    depelim Hsp.
    eapply ws_cumul_pb_Ind_l_inv in w as [i'' [args'' [? ?]]]; auto.
    eapply invert_red_mkApps_tInd in c as [? [eq ?]]; auto. solve_discr.
    ∃ nil.
    split; pcuic. clear i0.
    relativize (map (subst0 []) args).
    2:rewrite subst_empty_eq map_id //. clear i1.
    revert args' a0. clear -wfΣ wfΓ a.
    induction a; intros args' H; depelim H; constructor.
    transitivity y; auto. symmetry.
    now eapply red_conv. now eauto.
    now eapply invert_cumul_ind_prod in w.
  - intros d Γ' IH args args' ind i ind' i' inst wat Hsp.
    rewrite it_mkProd_or_LetIn_app in Hsp.
    destruct d as [na [b|] ty]; simpl in *; rewrite /mkProd_or_LetIn /= in Hsp.
    + rewrite context_assumptions_app /= Nat.add_0_r.
      eapply typing_spine_letin_inv in Hsp; auto.
      rewrite /subst1 subst_it_mkProd_or_LetIn /= in Hsp.
      specialize (IH (subst_context [b] 0 Γ')).
      forward IH by rewrite subst_context_length; lia.
      rewrite subst_mkApps Nat.add_0_r in Hsp.
      specialize (IH (map (subst [b] #|Γ'|) args) args' ind i ind' i' inst).
      forward IH. {
        move: wat; rewrite it_mkProd_or_LetIn_app /= /mkProd_or_LetIn /= ⇒ wat.
        eapply isType_tLetIn_red in wat; auto.
        now rewrite /subst1 subst_it_mkProd_or_LetIn subst_mkApps Nat.add_0_r
        in wat. }
      rewrite context_assumptions_subst in IH.
      intuition auto.
      destruct X as [isub [Hisub Hinst Hind Hi Hargs Hs]].
      eexists. split; auto.
      eapply make_context_subst_spec in Hisub.
      eapply make_context_subst_spec_inv.
      rewrite List.rev_app_distr. simpl.
      rewrite List.rev_involutive.
      eapply (context_subst_subst [{| decl_name := na; decl_body := Some b; decl_type := ty |}] [] [b] Γ').
      rewrite -{2} (subst_empty 0 b). eapply context_subst_def. constructor.
      now rewrite List.rev_involutive in Hisub.
      now len in Hi.
      rewrite map_map_compose in Hargs.
      assert (map (subst0 isub ∘ subst [b] #|Γ'|) args = map (subst0 (isub ++ [b])) args) as <-.
      { eapply map_ext ⇒ x. simpl.
        assert(#|Γ'| = #|isub|).
        { apply make_context_subst_spec in Hisub.
          apply context_subst_length in Hisub.
          now rewrite List.rev_involutive subst_context_length in Hisub. }
        rewrite H.
        now rewrite -(subst_app_simpl isub [b] 0). }
      exact Hargs.
      eapply subslet_app; eauto. rewrite -{1}(subst_empty 0 b). repeat constructor.
      rewrite !subst_empty.
      rewrite it_mkProd_or_LetIn_app /= /mkProd_or_LetIn /= in wat.
      now eapply isType_tLetIn_dom in wat.
    + rewrite context_assumptions_app /=.
      pose proof (typing_spine_WAT_concl Hsp).
      depelim Hsp; [now eapply invert_cumul_prod_ind in w|].
      eapply ws_cumul_pb_Prod_Prod_inv in w as [eqna conva cumulB].
      eapply (substitution_ws_cumul_pb (Γ' := [_]) (Γ'' := []) (s := [hd])) in cumulB; auto.
      rewrite /subst1 subst_it_mkProd_or_LetIn /= in cumulB.
      specialize (IH (subst_context [hd] 0 Γ')).
      forward IH by rewrite subst_context_length; lia.
      specialize (IH (map (subst [hd] #|Γ'|) args) args' ind i ind' i' tl). all:auto.
      have isTypes: isType Σ Γ
      (it_mkProd_or_LetIn (subst_context [hd] 0 Γ')
          (mkApps (tInd ind i) (map (subst [hd] #|Γ'|) args))). {
        move: wat; rewrite it_mkProd_or_LetIn_app /= /mkProd_or_LetIn /= ⇒ wat.
        eapply isType_tProd in wat as [isty wat].
        eapply (isType_subst (Δ := [_]) [hd]) in wat.
        now rewrite subst_it_mkProd_or_LetIn Nat.add_0_r subst_mkApps in wat.
        eapply subslet_ass_tip. eapply type_ws_cumul_pb; tea. now symmetry. }
      rewrite subst_mkApps Nat.add_0_r in cumulB. simpl in ×.
      rewrite context_assumptions_subst in IH.
      eapply typing_spine_strengthen in Hsp.
      3:eapply cumulB. all:eauto.
      intuition auto.
      destruct X1 as [isub [Hisub Htl Hind Hu Hargs Hs]].
      ∃ (isub ++ [hd]). rewrite List.rev_app_distr.
      len in Hu.
      split; auto. 2:lia.
      × apply make_context_subst_spec_inv.
        apply make_context_subst_spec in Hisub.
        rewrite List.rev_app_distr !List.rev_involutive in Hisub |- ×.
        eapply (context_subst_subst [{| decl_name := na; decl_body := None; decl_type := ty |}] [hd] [hd] Γ'); auto.
        eapply (context_subst_ass _ [] []). constructor.
      × assert (map (subst0 isub ∘ subst [hd] #|Γ'|) args = map (subst0 (isub ++ [hd])) args) as <-.
      { eapply map_ext ⇒ x. simpl.
        assert(#|Γ'| = #|isub|).
        { apply make_context_subst_spec in Hisub.
          apply context_subst_length in Hisub.
          now rewrite List.rev_involutive subst_context_length in Hisub. }
        rewrite H.
        now rewrite -(subst_app_simpl isub [hd] 0). }
        now rewrite map_map_compose in Hargs.
      × eapply subslet_app; auto.
        constructor. constructor. rewrite subst_empty.
        rewrite it_mkProd_or_LetIn_app /= /mkProd_or_LetIn /= in wat.
        eapply isType_tProd in wat as [Hty _]; auto.
        eapply type_ws_cumul_pb; eauto. now eapply ws_cumul_pb_eq_le.
      × pcuic.
Qed.

Lemma wf_cofixpoint_typing_spine {cf:checker_flags} (Σ : global_env_ext) Γ ind u mfix idx d args args' :
  wf Σ.1 → wf_local Σ Γ →
  wf_cofixpoint Σ mfix →
  nth_error mfix idx = Some d →
  isType Σ Γ (dtype d) →
  typing_spine Σ Γ (dtype d) args (mkApps (tInd ind u) args') →
  check_recursivity_kind (lookup_env Σ) (inductive_mind ind) CoFinite.
Proof.
  intros wfΣ wfΓ wfcofix Hnth wat sp.
  apply wf_cofixpoint_all in wfcofix.
  destruct wfcofix as [mind [cr allfix]].
  eapply nth_error_all in allfix; eauto.
  simpl in allfix.
  destruct allfix as [ctx [i [u' [args'' eqty]]]].
  rewrite {}eqty in sp wat.
  eapply mkApps_ind_typing_spine in sp; auto.
  destruct sp as [instsub [makes Hargs Hind Hu subs subsl]].
  now subst ind.
Qed.

Lemma Construct_Ind_ind_eq {cf:checker_flags} {Σ} (wfΣ : wf Σ.1):
  ∀ {Γ n i args u i' args' u' mdecl idecl cdecl},
  Σ ;;; Γ |- mkApps (tConstruct i n u) args : mkApps (tInd i' u') args' →
  declared_constructor Σ.1 (i, n) mdecl idecl cdecl →
  (i = i') ×
  
  R_ind_universes Σ i (context_assumptions (ind_params mdecl) + #|cstr_indices cdecl|) u u' ×
  consistent_instance_ext Σ (ind_universes mdecl) u ×
  consistent_instance_ext Σ (ind_universes mdecl) u' ×
  (#|args| = (ind_npars mdecl + context_assumptions cdecl.(cstr_args))%nat) ×
  ∑ parsubst argsubst parsubst' argsubst',
    let parctx := (subst_instance u (ind_params mdecl)) in
    let parctx' := (subst_instance u' (ind_params mdecl)) in
    let argctx := (subst_context parsubst 0
    ((subst_context (inds (inductive_mind i) u mdecl.(ind_bodies)) #|ind_params mdecl|
    (subst_instance u cdecl.(cstr_args))))) in
    let argctx2 := (subst_context parsubst' 0
    ((subst_context (inds (inductive_mind i) u' mdecl.(ind_bodies)) #|ind_params mdecl|
    (subst_instance u' cdecl.(cstr_args))))) in
    let argctx' := (subst_context parsubst' 0 (subst_instance u' idecl.(ind_indices))) in
    
    [× spine_subst Σ Γ (firstn (ind_npars mdecl) args) parsubst parctx,
    spine_subst Σ Γ (firstn (ind_npars mdecl) args') parsubst' parctx',
    spine_subst Σ Γ (skipn (ind_npars mdecl) args) argsubst argctx,
    spine_subst Σ Γ (skipn (ind_npars mdecl) args') argsubst' argctx' &
    ∑ s,
      sorts_local_ctx (lift_typing typing) Σ Γ argctx2 s ×
      

      ws_cumul_pb_terms Σ Γ (firstn mdecl.(ind_npars) args) (firstn mdecl.(ind_npars) args') ×

    

    ws_cumul_pb_terms Σ Γ
      (map (subst0 (argsubst ++ parsubst) ∘
      subst (inds (inductive_mind i) u mdecl.(ind_bodies)) (#|cdecl.(cstr_args)| + #|ind_params mdecl|)
      ∘ (subst_instance u))
        cdecl.(cstr_indices))
      (skipn mdecl.(ind_npars) args') ].
Proof.
  intros Γ n i args u i' args' u' mdecl idecl cdecl h declc.
  destruct (on_declared_constructor declc) as [[onmind onind] [? [_ onc]]].
  pose proof (validity h) as vi'.
  eapply inversion_mkApps in h; auto.
  destruct h as [T [hC hs]].
  apply inversion_Construct in hC
    as [mdecl' [idecl' [cdecl' [hΓ [isdecl [const htc]]]]]]; auto.
  assert (vty:=declared_constructor_valid_ty _ _ _ _ _ _ _ _ wfΣ hΓ isdecl const).
  eapply typing_spine_strengthen in hs. 3:eapply htc. all:eauto.
  destruct (declared_constructor_inj isdecl declc) as [? [? ?]].
  subst mdecl' idecl' cdecl'. clear isdecl.
  pose proof (on_constructor_inst declc _ const).
  destruct declc as [decli declc].
  destruct onc as [argslength cdecl_eq [cs' t] cargs cinds]; simpl.
  simpl in ×.
  unfold type_of_constructor in hs. simpl in hs.
  rewrite cdecl_eq in hs.
  rewrite !subst_instance_it_mkProd_or_LetIn in hs.
  rewrite !subst_it_mkProd_or_LetIn subst_instance_length Nat.add_0_r in hs.
  rewrite subst_instance_mkApps subst_mkApps subst_instance_length in hs.
  assert (Hind : inductive_ind i < #|ind_bodies mdecl|).
  { destruct decli.
    now eapply nth_error_Some_length in H0. }
  rewrite (subst_inds_concl_head i) in hs ⇒ //.
  rewrite -it_mkProd_or_LetIn_app in hs.
  assert(ind_npars mdecl = context_assumptions (ind_params mdecl)).
  { now pose (onNpars onmind). }
  assert (closed_ctx (ind_params mdecl)).
  { destruct onmind.
    red in onParams. now apply closed_wf_local in onParams. }
  eapply mkApps_ind_typing_spine in hs as [isubst [Hisubst Hargslen Hi Hu Hargs Hs]]; auto.
  subst i'.
  eapply (isType_mkApps_Ind_inv wfΣ decli) in vi' as (parsubst & argsubst & [spars sargs parlen argslen cons]) ⇒ //.
  split⇒ //. split⇒ //.
  split; auto. split ⇒ //.
  now len in Hu.
  now rewrite Hargslen context_assumptions_app !context_assumptions_subst !context_assumptions_subst_instance; lia.

  ∃ (skipn #|cdecl.(cstr_args)| isubst), (firstn #|cdecl.(cstr_args)| isubst).
  apply make_context_subst_spec in Hisubst.
  move: Hisubst.
  rewrite List.rev_involutive.
  move/context_subst_app.
  rewrite !subst_context_length !subst_instance_length.
  rewrite context_assumptions_subst context_assumptions_subst_instance -H.
  move⇒ [argsub parsub].
  rewrite closed_ctx_subst in parsub.
  now rewrite closedn_subst_instance_context.
  eapply subslet_app_inv in Hs.
  move: Hs. len. intuition auto.
  rewrite closed_ctx_subst in a0 ⇒ //.
  now rewrite closedn_subst_instance_context.

  ∃ parsubst, argsubst.
  assert(wfar : wf_local Σ
  (Γ ,,, subst_instance u' (arities_context (ind_bodies mdecl)))).
  { eapply weaken_wf_local ⇒ //.
    eapply wf_local_instantiate ⇒ //; destruct decli; eauto.
    eapply wf_arities_context ⇒ //; eauto. }
  assert(wfpars : wf_local Σ (subst_instance u (ind_params mdecl))).
    { eapply on_minductive_wf_params ⇒ //; eauto. }

  split; auto; try split; auto.
  - apply weaken_wf_local ⇒ //.
  - pose proof (subslet_length a0). rewrite subst_instance_length in H1.
    rewrite -H1 -subst_app_context.
    eapply (substitution_wf_local (Γ' := subst_instance u (arities_context (ind_bodies mdecl) ,,, ind_params mdecl))); eauto.
    rewrite subst_instance_app; eapply subslet_app; eauto.
    now rewrite closed_ctx_subst ?closedn_subst_instance_context.
    eapply (weaken_subslet (Γ' := [])) ⇒ //.
    now eapply subslet_inds; eauto.
    rewrite -app_context_assoc.
    eapply weaken_wf_local ⇒ //.
    rewrite -subst_instance_app_ctx.
    apply a.
  - ∃ (map (subst_instance_univ u') x). split.
    × move/onParams: onmind. rewrite /on_context.
      pose proof (@wf_local_instantiate _ Σ (InductiveDecl mdecl) (ind_params mdecl) u').
      move⇒ H'. eapply X in H'; eauto.
      2:destruct decli; eauto.
      clear -wfar wfpars wfΣ hΓ cons decli t cargs sargs H0 H' a spars a0.
      eapply (subst_sorts_local_ctx (Γ' := [])
      (Δ := subst_context (inds (inductive_mind i) u' (ind_bodies mdecl)) 0
        (subst_instance u' (ind_params mdecl)))) ⇒ //.
      simpl. eapply weaken_wf_local ⇒ //.
      rewrite closed_ctx_subst ⇒ //.
      now rewrite closedn_subst_instance_context.
      simpl. rewrite -(subst_instance_length u' (ind_params mdecl)).
      eapply (subst_sorts_local_ctx (Δ := subst_instance u' (arities_context (ind_bodies mdecl)))) ⇒ //.
      eapply weaken_wf_local ⇒ //.
      rewrite -app_context_assoc.
      eapply weaken_sorts_local_ctx ⇒ //.
      rewrite -subst_instance_app_ctx.
      eapply sorts_local_ctx_instantiate ⇒ //; destruct decli; eauto.
      eapply (weaken_subslet (Γ' := [])) ⇒ //.
      now eapply subslet_inds; eauto.
      rewrite closed_ctx_subst ?closedn_subst_instance_context. auto.
      apply spars.
    × move: (All2_firstn _ _ _ _ _ mdecl.(ind_npars) Hargs).
      move: (All2_skipn _ _ _ _ _ mdecl.(ind_npars) Hargs).
      clear Hargs.
      rewrite !map_map_compose !map_app.
      rewrite -map_map_compose.
      rewrite (firstn_app_left).
      { rewrite !map_length to_extended_list_k_length. lia. }
      rewrite skipn_all_app_eq ?lengths //.
      rewrite !map_map_compose.
      assert (#|cdecl.(cstr_args)| ≤ #|isubst|).
      apply context_subst_length in argsub.
      len in argsub.
      now apply firstn_length_le_inv.

      rewrite -(firstn_skipn #|cdecl.(cstr_args)| isubst).
      rewrite -[map _ (to_extended_list_k _ _)]
                (map_map_compose _ _ _ (subst_instance u)
                                (fun x ⇒ subst _ _ (subst _ _ x))).
      rewrite subst_instance_to_extended_list_k.
      rewrite -[map _ (to_extended_list_k _ _)]map_map_compose.
      rewrite -to_extended_list_k_map_subst.
      rewrite subst_instance_length. lia.
      rewrite map_subst_app_to_extended_list_k.
      rewrite firstn_length_le ⇒ //.

      erewrite subst_to_extended_list_k.
      rewrite map_lift0. split. eauto.
      rewrite firstn_skipn. rewrite firstn_skipn in All2_skipn.
      now rewrite firstn_skipn.

      apply make_context_subst_spec_inv. now rewrite List.rev_involutive.

  - rewrite it_mkProd_or_LetIn_app.
    unfold type_of_constructor in vty.
    rewrite cdecl_eq in vty. move: vty.
    rewrite !subst_instance_it_mkProd_or_LetIn.
    rewrite !subst_it_mkProd_or_LetIn subst_instance_length Nat.add_0_r.
    rewrite subst_instance_mkApps subst_mkApps subst_instance_length.
    rewrite subst_inds_concl_head. all:simpl; auto.
Qed.

Lemma Construct_Ind_ind_eq' {cf:checker_flags} {Σ} (wfΣ : wf Σ.1):
  ∀ {Γ n i args u i' args' u' },
  Σ ;;; Γ |- mkApps (tConstruct i n u) args : mkApps (tInd i' u') args' →
  ∑ mdecl idecl cdecl,
  declared_constructor Σ.1 (i, n) mdecl idecl cdecl ×
  (i = i') ×
  
  R_ind_universes Σ i (context_assumptions (ind_params mdecl) + #|cstr_indices cdecl|) u u' ×
  consistent_instance_ext Σ (ind_universes mdecl) u ×
  consistent_instance_ext Σ (ind_universes mdecl) u' ×
  (#|args| = (ind_npars mdecl + context_assumptions cdecl.(cstr_args))%nat) ×
  ∑ parsubst argsubst parsubst' argsubst',
    let parctx := (subst_instance u (ind_params mdecl)) in
    let parctx' := (subst_instance u' (ind_params mdecl)) in
    let argctx := (subst_context parsubst 0
    ((subst_context (inds (inductive_mind i) u mdecl.(ind_bodies)) #|ind_params mdecl|
    (subst_instance u cdecl.(cstr_args))))) in
    let argctx2 := (subst_context parsubst' 0
    ((subst_context (inds (inductive_mind i) u' mdecl.(ind_bodies)) #|ind_params mdecl|
    (subst_instance u' cdecl.(cstr_args))))) in
    let argctx' := (subst_context parsubst' 0 (subst_instance u' idecl.(ind_indices))) in
    
    [× spine_subst Σ Γ (firstn (ind_npars mdecl) args) parsubst parctx,
    spine_subst Σ Γ (firstn (ind_npars mdecl) args') parsubst' parctx',
    spine_subst Σ Γ (skipn (ind_npars mdecl) args) argsubst argctx,
    spine_subst Σ Γ (skipn (ind_npars mdecl) args') argsubst' argctx' &
    ∑ s,
      sorts_local_ctx (lift_typing typing) Σ Γ argctx2 s ×
      

      ws_cumul_pb_terms Σ Γ (firstn mdecl.(ind_npars) args) (firstn mdecl.(ind_npars) args') ×

    

    ws_cumul_pb_terms Σ Γ
      (map (subst0 (argsubst ++ parsubst) ∘
      subst (inds (inductive_mind i) u mdecl.(ind_bodies)) (#|cdecl.(cstr_args)| + #|ind_params mdecl|)
      ∘ (subst_instance u))
        cdecl.(cstr_indices))
      (skipn mdecl.(ind_npars) args') ].
Proof.
  intros Γ n i args u i' args' u' X.
  eapply inversion_mkApps in X as X'. destruct X' as (? & X' & _).
  eapply inversion_Construct in X' as (mdecl & idecl & cdecl & ? & ? & ? & ?); eauto.
  ∃ mdecl, idecl, cdecl. split; eauto.
  eapply Construct_Ind_ind_eq; eauto.
Qed.

Notation "⋆" := ltac:(solve [pcuic]) (only parsing).

Notation decl_ws_cumul_pb Σ Γ := (All_decls_alpha_pb Conv
  (fun pb (x0 y0 : term) ⇒ Σ ;;; Γ ⊢ x0 ≤[pb] y0)).

Lemma conv_decls_fix_context_gen {cf:checker_flags} Σ Γ mfix mfix1 :
  wf Σ.1 →
  All2 (fun d d' ⇒ Σ ;;; Γ ⊢ d.(dtype) = d'.(dtype) × eq_binder_annot d.(dname) d'.(dname)) mfix mfix1 →
  ∀ Γ' Γ'',
  Σ ⊢ Γ ,,, Γ' = Γ ,,, Γ'' →
  ws_cumul_ctx_pb_rel Conv Σ (Γ ,,, Γ') (fix_context_gen #|Γ'| mfix) (fix_context_gen #|Γ''| mfix1).
Proof.
  intros wfΣ a Γ' Γ'' convctx.
  split. eauto with fvs.
  induction a in Γ', Γ'', convctx |- ×. constructor. simpl.
  destruct r as [r eqann].

  assert(decl_ws_cumul_pb Σ (Γ ,,, Γ' ,,, [])
    (vass (dname x) (lift0 #|Γ'| (dtype x)))
    (vass (dname y) (lift0 #|Γ''| (dtype y)))).
  { constructor; tas.
    pose proof (All2_fold_length convctx).
    rewrite !app_length in H. assert(#|Γ'| = #|Γ''|) by lia.
    rewrite -H0.
    apply (weakening_ws_cumul_pb (Γ' := [])); eauto with fvs. }

  apply All2_fold_app.
  constructor ⇒ //. constructor.
  eapply (All2_fold_impl (P:= (fun Δ Δ' : context ⇒
  decl_ws_cumul_pb Σ
    (Γ ,,, (vass (dname x) (lift0 #|Γ'| (dtype x)) :: Γ') ,,, Δ)))).
  eapply (IHa (vass _ _ :: Γ') (vass _ _ :: Γ'')).
  cbn; constructor ⇒ //. constructor; eauto.
  depelim X. eauto.
  intros. red.
  now rewrite ![_ ,,, _]app_context_assoc.
Qed.

Lemma conv_decls_fix_context {cf:checker_flags} {Σ} {wfΣ : wf Σ} {Γ mfix mfix1} :
  wf_local Σ Γ →
  All2 (fun d d' ⇒ Σ ;;; Γ ⊢ d.(dtype) = d'.(dtype) × eq_binder_annot d.(dname) d'.(dname)) mfix mfix1 →
  All2_fold (fun Δ Δ' : context ⇒ decl_ws_cumul_pb Σ (Γ ,,, Δ))
    (fix_context mfix) (fix_context mfix1).
Proof.
  intros wfΓ a.
  apply (conv_decls_fix_context_gen _ _ _ _ wfΣ a [] []).
  eapply ws_cumul_ctx_pb_refl. eauto with fvs.
Qed.

Lemma isLambda_red1 Σ Γ b b' : isLambda b → red1 Σ Γ b b' → isLambda b'.
Proof.
  destruct b; simpl; try discriminate.
  intros _ red.
  depelim red.
  symmetry in H; apply mkApps_Fix_spec in H. simpl in H. intuition.
  constructor. constructor.
Qed.

Lemma declared_inductive_unique {Σ mdecl idecl p} (q r : declared_inductive Σ p mdecl idecl) : q = r.
Proof.
  unfold declared_inductive in q, r.
  destruct q, r.
  now rewrite (uip e e0) (uip d d0).
Qed.

Lemma declared_inductive_unique_sig {cf:checker_flags} {Σ ind mib decl mib' decl'}
      (decl1 : declared_inductive Σ ind mib decl)
      (decl2 : declared_inductive Σ ind mib' decl') :
  @sigmaI _ (fun '(m, d) ⇒ declared_inductive Σ ind m d)
          (mib, decl) decl1 =
  @sigmaI _ _ (mib', decl') decl2.
Proof.
  pose proof (declared_inductive_inj decl1 decl2) as (<-&<-).
  pose proof (declared_inductive_unique decl1 decl2) as →.
  reflexivity.
Qed.

Lemma ws_cumul_ctx_pb_rel_context_assumptions {cf:checker_flags} P Γ Δ Δ' :
  ws_cumul_ctx_pb_rel Conv P Γ Δ Δ' →
  context_assumptions Δ = context_assumptions Δ'.
Proof.
  move⇒ [] _. induction 1; auto.
  cbn.
  depelim p; cbn; lia.
Qed.

Lemma invert_Case_Construct {cf:checker_flags} Σ (hΣ : ∥ wf Σ.1 ∥)
  {Γ ci ind' pred i u brs args T} :
  Σ ;;; Γ |- tCase ci pred (mkApps (tConstruct ind' i u) args) brs : T →
  ci.(ci_ind) = ind' ∧
  ∃ br,
    nth_error brs i = Some br ∧
    (#|args| = ci.(ci_npar) + context_assumptions br.(bcontext))%nat.
Proof.
  destruct hΣ as [wΣ].
  intros h.
  apply inversion_Case in h as ih ; auto.
  destruct ih
    as [mdecl [idecl [isdecl [indices [cinv cum]]]]].
  destruct cinv.
  pose proof scrut_ty as typec.
  eapply inversion_mkApps in typec as [A' [tyc tyargs]]; auto.
  eapply (inversion_Construct Σ wΣ) in tyc as [mdecl' [idecl' [cdecl' [wfl [declc [Hu tyc]]]]]].
  epose proof (PCUICInductiveInversion.Construct_Ind_ind_eq _ scrut_ty declc); eauto.
  simpl in ×.
  intuition auto.
  subst.
  destruct declc as (decli&nthctor).
  cbn in nthctor.
  pose proof (declared_inductive_unique_sig isdecl decli) as H; noconf H.
  eapply All2i_nth_error_l in nthctor as H; eauto.
  destruct H as (br & nth & cc & ? & ? &?).
  ∃ br.
  split; auto.
  cbn in cc.
  assert (context_assumptions (bcontext br) = context_assumptions (cstr_branch_context ci mdecl cdecl')).
  { clear -cc. induction cc; simpl; auto. destruct r; cbn; auto. lia. }
  rewrite H.
  unfold cstr_branch_context, expand_lets_ctx, expand_lets_k_ctx.
  repeat (rewrite ?context_assumptions_subst_context
                  ?context_assumptions_lift_context
                  ?context_assumptions_subst_instance).
  congruence.
Qed.

Lemma Proj_Construct_ind_eq {cf:checker_flags} Σ (hΣ : ∥ wf Σ.1 ∥) {Γ i' p c u l T} :
  Σ ;;; Γ |- tProj p (mkApps (tConstruct i' c u) l) : T →
  p.(proj_ind) = i'.
Proof.
  destruct hΣ as [wΣ].
  intros h.
  apply inversion_Proj in h ; auto.
  destruct h as [uni [mdecl [idecl [pdecl [args' [? [declp [hc [? ?]]]]]]]]].
  pose proof hc as typec.
  eapply inversion_mkApps in typec as [A' [tyc tyargs]]; auto.
  eapply (inversion_Construct Σ wΣ) in tyc as [mdecl' [idecl' [cdecl' [wfl [declc [Hu tyc]]]]]].
  epose proof (PCUICInductiveInversion.Construct_Ind_ind_eq _ hc declc); eauto.
  intuition auto.
Qed.

Lemma invert_Proj_Construct {cf:checker_flags} Σ (hΣ : ∥ wf Σ.1 ∥) {Γ p i' c u l T} :
  Σ ;;; Γ |- tProj p (mkApps (tConstruct i' c u) l) : T →
  p.(proj_ind) = i' ∧ c = 0 ∧ p.(proj_npars) + p.(proj_arg) < #|l|.
Proof.
  intros h.
  assert (h' := h).
  apply Proj_Construct_ind_eq in h' as <-; auto.
  destruct hΣ as [wΣ].
  split; [reflexivity|].
  apply inversion_Proj in h ; auto.
  destruct h as [uni [mdecl [idecl [pdecl [args' [? [declp [hc [? ?]]]]]]]]].
  pose proof hc as typec.
  eapply inversion_mkApps in typec as [A' [tyc tyargs]]; auto.
  eapply (inversion_Construct Σ wΣ) in tyc as [mdecl' [idecl' [cdecl' [wfl [declc [Hu tyc]]]]]].
  pose proof (declared_inductive_unique_sig declp.p1.p1 declc.p1) as H; noconf H.
  cbn in H.
  clear H.
  epose proof (PCUICInductiveInversion.Construct_Ind_ind_eq _ hc declc); eauto.
  simpl in X.
  destruct (on_declared_projection declp).
  set (oib := declared_inductive_inv _ _ _ _) in ×.
  simpl in ×.
  destruct declc.
  destruct p1 as [[[? ?] ?] ?].
  destruct p0.
  destruct (ind_cunivs oib) as [|? []] eqn:hctor in y; try contradiction.
  simpl in H. simpl in H0.
  rewrite e0 in H0.
  destruct c; simpl in H0 ⇒ //; noconf H0.
  intuition auto.
  2:{ rewrite nth_error_nil in H0. noconf H0. }
  rewrite b0.
  destruct declp as [decli [nthp parseq]].
  simpl in ×. rewrite parseq. lia.
Qed.
Notation "!! t" := ltac:(refine t) (at level 200, only parsing).

Lemma isType_mkApps_Ind_smash {cf:checker_flags} {Σ Γ ind u params args} {wfΣ : wf Σ} {mdecl idecl} :
  declared_inductive Σ.1 ind mdecl idecl →
  isType Σ Γ (mkApps (tInd ind u) (params ++ args)) →
  #|params| = ind_npars mdecl →
  let parctx := subst_instance u mdecl.(ind_params) in
  let argctx := subst_instance u idecl.(ind_indices) in
  spine_subst Σ Γ params (List.rev params) (smash_context [] parctx) ×
  spine_subst Σ Γ args (List.rev args) (smash_context [] (subst_context_let_expand (List.rev params) parctx argctx)) ×
  consistent_instance_ext Σ (ind_universes mdecl) u.
Proof.
  move⇒ isdecl isty hpars.
  pose proof (isType_wf_local isty).
  destruct isty as [s Hs].
  eapply invert_type_mkApps_ind in Hs as [sp cu]; tea.
  move⇒ parctx argctx.
  erewrite ind_arity_eq in sp.
  2: eapply PCUICInductives.oib ; eauto.
  rewrite !subst_instance_it_mkProd_or_LetIn in sp.
  rewrite -it_mkProd_or_LetIn_app /= in sp.
  eapply arity_typing_spine in sp as [hle hs [insts sp]]; tea.
  eapply spine_subst_smash in sp; tea.
  rewrite smash_context_app_expand in sp.
  rewrite List.rev_app_distr in sp.
  pose proof (declared_minductive_ind_npars isdecl) as hnpars.
  eapply spine_subst_app_inv in sp as [sppars spargs]; tea.
  2:{ rewrite context_assumptions_smash_context /=. len. }
  len in sppars. len in hle. len in spargs.
  simpl in ×.
  assert (context_assumptions (ind_indices idecl) = #|List.rev args|) by (len; lia).
  rewrite H skipn_all_app in sppars, spargs.
  split ⇒ //. split ⇒ //.
  rewrite -(Nat.add_0_r #|List.rev args|) firstn_app_2 firstn_0 // app_nil_r in spargs.
  rewrite (smash_context_subst []).
  rewrite -(expand_lets_smash_context _ []).
  exact spargs.
Qed.

Lemma instantiate_subslet {cf Σ} {Γ s Δ} {c} {decl : global_decl} {u : Instance.t} {wfΣ : wf Σ.1} :
  lookup_env Σ.1 c = Some decl →
        subslet (Σ.1, universes_decl_of_decl decl) Γ s Δ →
  consistent_instance_ext Σ (universes_decl_of_decl decl) u →
  subslet Σ Γ@[u] s@[u] Δ@[u].
Proof.
  intros hl subs cu.
  induction subs.
  - constructor.
  - cbn. constructor; auto.
    cbn. rewrite -subst_instance_subst. eapply typing_subst_instance_decl; tea.
  - cbn. rewrite subst_instance_subst. constructor; auto.
    cbn. rewrite - !subst_instance_subst.
    eapply typing_subst_instance_decl; tea.
Qed.

Lemma instantiate_wf_subslet {cf Σ} {Γ s Δ} {c} {decl : global_decl} {u : Instance.t} {wfΣ : wf Σ.1} :
  lookup_env Σ.1 c = Some decl →
        wf_subslet (Σ.1, universes_decl_of_decl decl) Γ s Δ →
  consistent_instance_ext Σ (universes_decl_of_decl decl) u →
  wf_subslet Σ Γ@[u] s@[u] Δ@[u].
Proof.
  intros hl [wf subs] cu.
  split.
  rewrite -subst_instance_app_ctx. eapply wf_local_instantiate; tea.
  now eapply instantiate_subslet.
Qed.

Lemma projection_context_gen_inst {cf} {Σ mdecl idecl ind u} :
  declared_inductive Σ.1 ind mdecl idecl →
  consistent_instance_ext Σ (ind_universes mdecl) u →
  (projection_context_gen ind mdecl idecl)@[u] =
  projection_context ind mdecl idecl u.
Proof.
  intros isdecl cu.
  rewrite /projection_context /projection_context_gen.
  rewrite /snoc /= -(subst_instance_smash _ _ []).
  cbn. f_equal. rewrite /map_decl /= /vass /=.
  f_equal. rewrite subst_instance_mkApps /=.
  rewrite subst_instance_to_extended_list. f_equal.
  cbn.
  now rewrite [subst_instance_instance _ _](subst_instance_id_mdecl _ _ _ cu).
Qed.

Lemma substitution_subslet {cf:checker_flags} {Σ} {wfΣ : wf Σ} {Γ Γ' Δ s s' Δ'} :
  subslet Σ Γ s Δ →
  wf_subslet Σ (Γ ,,, Δ ,,, Γ') s' Δ' →
  wf_subslet Σ (Γ ,,, subst_context s 0 Γ') (map (subst s #|Γ'|) s') (subst_context s #|Γ'| Δ').
Proof.
  intros subl [wf subs].
  split.
  { rewrite -app_context_assoc.
    relativize #|Γ'|.
    erewrite <-subst_context_app. 2:lia.
    eapply substitution_wf_local; tea.
    now rewrite app_context_assoc. }
  clear wf.
  induction subs in s, subl |- ×.
  × cbn. intros. constructor.
  × cbn. rewrite subst_context_snoc. constructor; auto.
    eapply substitution in t0; tea.
    cbn. rewrite -(subslet_length subs).
    now rewrite -distr_subst.
  × cbn. rewrite subst_context_snoc.
    eapply substitution in t0; tea.
    specialize (IHsubs _ subl).
    epose proof (cons_let_def _ _ _ _ _ _ _ IHsubs).
    rewrite !distr_subst in t0.
    specialize (X t0).
    rewrite -(subslet_length subs).
    now rewrite -distr_subst in X.
Qed.

Lemma weaken_wf_subslet {cf Σ} {wfΣ : wf Σ} s (Δ Γ Γ' : context) :
  wf_local Σ Γ →
  wf_subslet Σ Γ' s Δ →
  wf_subslet Σ (Γ,,, Γ') s Δ.
Proof.
  intros wfΓ [wf subs]. split.
  rewrite -app_context_assoc.
  eapply weaken_wf_local ⇒ //.
  eapply weaken_subslet; tea.
  now eapply All_local_env_app_inv in wf.
Qed.

Lemma on_projections_indices {mdecl i idecl cs} :
  on_projections mdecl (inductive_mind i) (inductive_ind i)
    idecl (ind_indices idecl) cs →
    idecl.(ind_indices) = [].
Proof.
  move/on_projs_noidx. destruct ind_indices; try discriminate; auto.
Qed.

Lemma subslet_projs {cf:checker_flags} {Σ} {wfΣ : wf Σ} {i mdecl idecl args} :
  declared_inductive Σ.1 i mdecl idecl →
  match ind_ctors idecl return Type with
  | [cs] ⇒
    on_projections mdecl (inductive_mind i) (inductive_ind i)
     idecl (ind_indices idecl) cs →
     ∀ Γ t u,
     let indsubst := inds (inductive_mind i) u (ind_bodies mdecl) in
     Σ;;; Γ |- t : mkApps (tInd i u) args →
     wf_subslet Σ Γ
      (projs_inst i (ind_npars mdecl) (context_assumptions (cstr_args cs)) t)
      (subst_context (List.rev args) 0
        (subst_context (extended_subst (ind_params mdecl)@[u] 0) 0
          (smash_context []
            (subst_context (inds (inductive_mind i) u (ind_bodies mdecl))
              #|ind_params mdecl| (subst_instance u (cstr_args cs))))))
  | _ ⇒ True
  end.
Proof.
  intros Hdecl.
  destruct ind_ctors as [|cs []] eqn:Heq; trivial.
  intros onp. simpl. intros Γ t u.
  rewrite (smash_context_subst []).
  assert (#|PCUICEnvironment.ind_projs idecl| ≥
  PCUICEnvironment.context_assumptions (cstr_args cs)).
  { destruct onp. lia. }
  intros Ht.
  epose proof (declared_projections_subslet _ Hdecl cs Heq onp _ (Nat.le_refl _)).
  have v := !!(validity Ht). eapply isType_mkApps_Ind_inv in v as [? [? []]]; tea; pcuic.
  eapply (instantiate_wf_subslet (decl:=InductiveDecl mdecl)) in X; tea. 2:apply Hdecl.
  move: X. rewrite Nat.sub_diag skipn_0.
  rewrite subst_instance_subst_context subst_instance_lift_context.
  rewrite subst_context_lift_context_comm //.
  rewrite (projection_context_gen_inst Hdecl) //.
  rewrite /projection_context.
  eapply spine_subst_smash in s.
  intros Hs.
  have wfΓ : wf_local Σ Γ by (eapply typing_wf_local; eauto).
  eapply weaken_wf_subslet in Hs;tea.
  eapply (substitution_subslet (Γ' := [_])) in Hs; tea.
  2:eapply s.
  move: Hs. cbn.
  rewrite subst_context_snoc /= /subst_decl /= /map_decl /= subst_mkApps /=.
  rewrite (spine_subst_subst_to_extended_list_k s).
  move: (on_projections_indices onp) ⇒ heq. rewrite heq in e0.
  cbn in e0.
  assert (#|args| = ind_npars mdecl).
  rewrite -(firstn_skipn (ind_npars mdecl) args) app_length e0 e //.
  rewrite firstn_all2 //. lia.
  move/(substitution_subslet (Γ := Γ) (Δ := [_]) (Γ' := []) (subslet_ass_tip Ht)).
  cbn.
  rewrite [(projs _ _ _)@[u]]projs_subst_instance projs_subst_above // subst_projs_inst.
  rewrite subst_instance_subst_context.
  rewrite instantiate_inds //. exact Hdecl.
  rewrite subst_context_lift_context_comm //.
  rewrite subst_context_lift_context_cancel //.
  rewrite subst_instance_extended_subst //.
  rewrite subst_instance_smash //.
Qed.

Ltac unf_env :=
  change PCUICEnvironment.it_mkProd_or_LetIn with it_mkProd_or_LetIn in *;
  change PCUICEnvironment.to_extended_list_k with to_extended_list_k in *;
  change PCUICEnvironment.ind_params with ind_params in ×.

Derive Signature for positive_cstr.

Lemma positive_cstr_it_mkProd_or_LetIn mdecl i Γ Δ t :
  positive_cstr mdecl i Γ (it_mkProd_or_LetIn Δ t) →
  All_local_env (fun Δ ty _ ⇒ positive_cstr_arg mdecl (Γ ,,, Δ) ty)
    (smash_context [] Δ) ×
  positive_cstr mdecl i (Γ ,,, smash_context [] Δ) (expand_lets Δ t).
Proof.
  revert Γ t; unfold expand_lets, expand_lets_k;
   induction Δ as [|[na [b|] ty] Δ] using ctx_length_rev_ind; intros Γ t.
  - simpl; intuition auto. now rewrite subst_empty lift0_id.
  - rewrite it_mkProd_or_LetIn_app /=; intros H; depelim H.
    solve_discr. rewrite smash_context_app_def.
    rewrite /subst1 subst_it_mkProd_or_LetIn in H.
    specialize (X (subst_context [b] 0 Δ) ltac:(len; lia) _ _ H).
    simpl; len in X. len.
    destruct X; split; auto. simpl.
    rewrite extended_subst_app /= !subst_empty !lift0_id lift0_context.
    rewrite subst_app_simpl; len ⇒ /=.
    simpl.
    epose proof (distr_lift_subst_rec _ [b] (context_assumptions Δ) #|Δ| 0).
    rewrite !Nat.add_0_r in H0. now erewrite <- H0.
  - rewrite it_mkProd_or_LetIn_app /=; intros H; depelim H.
    solve_discr. rewrite smash_context_app_ass.
    specialize (X Δ ltac:(len; lia) _ _ H).
    simpl; len.
    destruct X; split; auto. simpl.
    eapply All_local_env_app; split.
    constructor; auto.
    eapply (All_local_env_impl _ _ _ a). intros; auto.
    now rewrite app_context_assoc. simpl.
    rewrite extended_subst_app /=.
    rewrite subst_app_simpl; len ⇒ /=.
    simpl.
    rewrite subst_context_lift_id.
    rewrite Nat.add_comm Nat.add_1_r subst_reli_lift_id.
    apply context_assumptions_length_bound. now rewrite app_context_assoc.
Qed.

Lemma expand_lets_k_app (Γ Γ' : context) t k : expand_lets_k (Γ ++ Γ') k t =
  expand_lets_k Γ' (k + context_assumptions Γ) (expand_lets_k Γ k t).
Proof.
  revert Γ k t.
  induction Γ' as [|[na [b|] ty] Γ'] using ctx_length_rev_ind; intros Γ k t.
  - simpl. now rewrite /expand_lets_k /= subst_empty lift0_id app_nil_r.
  - simpl; rewrite app_assoc !expand_lets_k_vdef /=; len; simpl.
    rewrite subst_context_app. specialize (H (subst_context [b] 0 Γ') ltac:(now len)).
    specialize (H (subst_context [b] #|Γ'| Γ)). rewrite Nat.add_0_r /app_context H; len.
    f_equal.
    rewrite /expand_lets_k; len.
    rewrite -Nat.add_assoc.
    rewrite distr_subst_rec; len.
    epose proof (subst_extended_subst_k [b] Γ #|Γ'| 0).
    rewrite Nat.add_0_r Nat.add_comm in H0. rewrite -H0. f_equal.
    rewrite commut_lift_subst_rec. lia. lia_f_equal.
  - simpl. rewrite app_assoc !expand_lets_k_vass /=; len; simpl.
    now rewrite (H Γ' ltac:(reflexivity)).
Qed.

Lemma expand_lets_app Γ Γ' t : expand_lets (Γ ++ Γ') t =
  expand_lets_k Γ' (context_assumptions Γ) (expand_lets Γ t).
Proof.
  now rewrite /expand_lets expand_lets_k_app.
Qed.

Lemma closedn_expand Γ Δ x :
  closed_ctx Γ →
  closedn (context_assumptions Δ + #|Γ|) (expand_lets Δ x) =
  closedn (context_assumptions Δ + context_assumptions Γ) (expand_lets (Γ ,,, Δ) x).
Proof.
  intros clΓ.
  rewrite /expand_lets.
  rewrite expand_lets_k_app /=.
  relativize (context_assumptions Δ + context_assumptions Γ).
  erewrite (closedn_expand_lets_eq 0) ⇒ /= //. now cbn.
Qed.

Lemma closedn_expand' (Γ Δ : context) x :
  closedn_ctx #|Γ| Δ →
  closedn (context_assumptions Δ + #|Γ|) (expand_lets Δ x) →
  closedn (#|Δ| + #|Γ|) x.
Proof.
  intros clΓ cl.
  eapply closed_upwards in cl.
  move: cl.
  rewrite /expand_lets.
  erewrite (closedn_expand_lets_eq #|Γ|) ⇒ /= //.
  now rewrite Nat.add_0_r Nat.add_comm.
  lia.
Qed.

Lemma positive_cstr_closed_indices {cf} {Σ} {wfΣ : wf Σ} :
  ∀ {i mdecl idecl cdecl},
  declared_constructor Σ.1 i mdecl idecl cdecl →
  All (closedn (context_assumptions (cstr_args cdecl) + #|ind_params mdecl|))
    (map (expand_lets (cstr_args cdecl)) (cstr_indices cdecl)).
Proof.
  intros.
  pose proof (on_declared_constructor H) as [[onmind oib] [cs [hnth onc]]].
  pose proof (onc.(on_ctype_positive)).
  rewrite onc.(cstr_eq) in X. unf_env.
  rewrite -it_mkProd_or_LetIn_app in X.
  eapply positive_cstr_it_mkProd_or_LetIn in X as [hpars hpos].
  rewrite app_context_nil_l in hpos.
  rewrite expand_lets_mkApps in hpos.
  unfold cstr_concl_head in hpos.
  have subsrel := expand_lets_tRel (#|ind_bodies mdecl| - S (inductive_ind i.1))
    (ind_params mdecl ,,, cstr_args cdecl). len in subsrel.
  rewrite (Nat.add_comm #|cstr_args cdecl|) Nat.add_assoc in subsrel.
  rewrite {}subsrel in hpos.
  depelim hpos; solve_discr.
  eapply All_map_inv in a.
  eapply All_app in a as [ _ a].
  eapply All_map; eapply (All_impl a); intros x; len.
  rewrite closedn_expand //.
  exact (declared_inductive_closed_params H).
Qed.

Lemma positive_cstr_arg_subst_instance {mdecl Γ} {t} u :
  positive_cstr_arg mdecl Γ t →
  positive_cstr_arg mdecl (subst_instance u Γ) (subst_instance u t).
Proof.
  induction 1.
  - constructor 1; len.
    now rewrite closedn_subst_instance.
  - rewrite subst_instance_mkApps. econstructor 2; len ⇒ //; eauto.
    eapply All_map; solve_all.
    now rewrite closedn_subst_instance.
  - simpl. constructor 3; len ⇒ //.
    now rewrite subst_instance_subst in IHX.
  - simpl. constructor 4; len ⇒ //.
    now rewrite closedn_subst_instance.
Qed.

Import ssrbool.

Lemma invert_red_mkApps_tRel {cf} {Σ} {wfΣ : wf Σ} {Γ n d args t'} :
  nth_error Γ n = Some d → decl_body d = None →
  Σ ;;; Γ ⊢ mkApps (tRel n) args ⇝ t' →
  ∑ args' : list term, t' = mkApps (tRel n) args' × red_terms Σ Γ args args'.
Proof.
  move⇒ hnth db [onΓ ont red].
  destruct Σ.
  move: ont. rewrite PCUICOnFreeVars.on_free_vars_mkApps /= ⇒ /andP[] // ⇒ onn onargs.
  unshelve eapply (red_mkApps_tRel (Γ := exist Γ onΓ) _ hnth db) in red as [args' [eq redargs]] ⇒ //.
  now cbn.
  ∃ args'; split ⇒ //.
  cbn in redargs. solve_all.
  eapply into_closed_red; eauto.
Qed.

Lemma ws_cumul_pb_mkApps_tRel {cf} {Σ} {wfΣ : wf Σ} {Γ n d u u'} :
  nth_error Γ n = Some d → decl_body d = None →
  Σ ;;; Γ ⊢ mkApps (tRel n) u ≤ mkApps (tRel n) u' →
  ws_cumul_pb_terms Σ Γ u u'.
Proof.
  intros Hnth Hd cum.
  pose proof (ws_cumul_pb_is_closed_context cum).
  eapply ws_cumul_pb_red in cum as [v' [v [redl redr leq]]].
  eapply invert_red_mkApps_tRel in redl as [args' [-> conv]]; eauto.
  eapply invert_red_mkApps_tRel in redr as [args'' [-> conv']]; eauto.
  eapply All2_trans. apply _.
  now eapply red_terms_ws_cumul_pb_terms.
  eapply eq_term_upto_univ_mkApps_l_inv in leq as [u'' [l' [[eqrel eqargs] eq']]].
  depelim eqrel. eapply mkApps_eq_inj in eq' as [_ ->] ⇒ //.
  etransitivity; [|symmetry; eapply red_terms_ws_cumul_pb_terms]; eauto.
  eapply closed_red_terms_open_right in conv.
  eapply closed_red_terms_open_right in conv'.
  eapply eq_terms_ws_cumul_pb_terms; eauto.
  all:solve_all.
Qed.

Lemma nth_error_subst_instance u Γ n :
  nth_error (subst_instance u Γ) n =
  option_map (map_decl (subst_instance u)) (nth_error Γ n).
Proof.
  now rewrite nth_error_map.
Qed.

Lemma ws_cumul_pb_terms_confl {cf} {Σ} {wfΣ : wf Σ} {Γ u u'} :
  ws_cumul_pb_terms Σ Γ u u' →
  ∑ nf nf', (red_terms Σ Γ u nf × red_terms Σ Γ u' nf') × (All2 (eq_term Σ Σ) nf nf').
Proof.
  intros cv.
  induction cv.
  - ∃ [], []; intuition auto.
  - destruct IHcv as [nf [nf' [[redl redr] eq]]].
    eapply ws_cumul_pb_red in r as [x' [y' [redx redy eq']]].
    ∃ (x' :: nf), (y' :: nf'); intuition auto.
Qed.

Lemma closed_red_mkApps {cf} {Σ} {wfΣ : wf Σ} Γ f u u' :
  is_closed_context Γ →
  is_open_term Γ f →
  red_terms Σ Γ u u' →
  Σ ;;; Γ ⊢ mkApps f u ⇝ mkApps f u'.
Proof.
  intros onΓ ont red.
  eapply into_closed_red; auto.
  - apply red_mkApps; auto.
    solve_all. apply X.
  - rewrite PCUICOnFreeVars.on_free_vars_mkApps ont.
    eapply closed_red_terms_open_left in red; solve_all.
Qed.

Lemma ws_cumul_pb_mkApps_eq {cf} {Σ} {wfΣ : wf Σ} Γ f f' u u' :
  is_closed_context Γ →
  is_open_term Γ f →
  is_open_term Γ f' →
  eq_term_upto_univ_napp Σ (eq_universe Σ) (leq_universe Σ) #|u| f f' →
  ws_cumul_pb_terms Σ Γ u u' →
  Σ ;;; Γ ⊢ mkApps f u ≤ mkApps f' u'.
Proof.
  intros onΓ onf onf' eqf equ.
  eapply ws_cumul_pb_red.
  eapply ws_cumul_pb_terms_confl in equ as [nf [nf' [[redl redr] eq]]] ⇒ //.
  ∃ (mkApps f nf), (mkApps f' nf').
  split.
  eapply closed_red_mkApps; eauto.
  eapply closed_red_mkApps; eauto.
  eapply eq_term_upto_univ_napp_mkApps.
  now rewrite Nat.add_0_r -(All2_length redl).
  apply eq.
Qed.

Lemma ws_cumul_pb_LetIn_inv {cf} {Σ} {wfΣ : wf Σ} {le Γ na na' b b' ty ty' t t'} :
  Σ ;;; Γ ⊢ tLetIn na b ty t ≤[le] tLetIn na' b' ty' t' →
  Σ ;;; Γ ⊢ t {0 := b} ≤[le] t' {0 := b'}.
Proof.
  intros cum.
  eapply ws_cumul_pb_LetIn_l_inv; eauto.
  eapply ws_cumul_pb_LetIn_r_inv; eauto.
Qed.

Lemma ws_cumul_pb_LetIn_subst {cf} {Σ} {wfΣ : wf Σ} {le Γ na na' b b' ty ty' t t'} :
  is_open_term Γ (tLetIn na b ty t) →
  is_open_term Γ (tLetIn na' b' ty' t') →
  Σ ;;; Γ ⊢ t {0 := b} ≤[le] t' {0 := b'} →
  Σ ;;; Γ ⊢ tLetIn na b ty t ≤[le] tLetIn na' b' ty' t'.
Proof.
  intros onl onr cum.
  transitivity (t {0 := b}).
  eapply red_ws_cumul_pb. eapply into_closed_red; eauto.
  eapply red1_red. econstructor. eauto with fvs.
  transitivity (t' {0 := b'}) ⇒ //.
  eapply red_ws_cumul_pb_inv.
  eapply into_closed_red; eauto.
  eapply red1_red; econstructor. eauto with fvs.
Qed.

Lemma ws_cumul_pb_Prod_Prod_inv_l {cf} {Σ} {wfΣ : wf Σ} Γ na na' A B A' B' :
  Σ ;;; Γ ⊢ tProd na A B ≤ tProd na' A' B' →
  [× eq_binder_annot na na', Σ ;;; Γ ⊢ A = A' & Σ ;;; Γ ,, vass na A ⊢ B ≤ B'].
Proof.
  move/ws_cumul_pb_Prod_Prod_inv ⇒ []; split; auto.
  eapply ws_cumul_pb_ws_cumul_ctx; tea.
  constructor; auto. eapply ws_cumul_ctx_pb_refl. eauto with fvs.
  constructor; auto. exact p0.
Qed.

Lemma inds_is_open_terms (Γ : context) ind mdecl u :
  forallb (is_open_term Γ) (inds (inductive_mind ind) u (ind_bodies mdecl)).
Proof.
  move: (@closed_inds ind mdecl u).
  eapply forallb_impl. intros x _.
  rewrite -is_open_term_closed // ⇒ cl.
  eapply closed_upwards; tea; auto. len.
Qed.

Lemma inds_nth_error ind u l n t :
  nth_error (inds ind u l) n = Some t → ∑ n, t = tInd {| inductive_mind := ind ; inductive_ind := n |} u.
Proof.
  unfold inds in ×. generalize (#|l|). clear. revert t.
  induction n; intros.
  - destruct n. cbn in H. congruence. cbn in H. inv H.
    eauto.
  - destruct n0. cbn in H. congruence. cbn in H.
    eapply IHn. eauto.
Qed.

Lemma positive_cstr_arg_subst {cf} {Σ} {wfΣ : wf Σ} {ind mdecl idecl Γ t u u'} :
  declared_inductive Σ ind mdecl idecl →
  consistent_instance_ext Σ (ind_universes mdecl) u →
  R_opt_variance (eq_universe Σ) (leq_universe Σ) (ind_variance mdecl) u u' →
  closed_ctx (ind_arities mdecl ,,, Γ)@[u] →
  Σ ;;; subst_instance u (ind_arities mdecl) ,,, subst_instance u Γ ⊢ (subst_instance u t) ≤ (subst_instance u' t) →
  positive_cstr_arg mdecl Γ t →
  (Σ ;;; subst_context (ind_subst mdecl ind u) 0 (subst_instance u Γ) ⊢
    (subst (ind_subst mdecl ind u) #|Γ| (subst_instance u t)) ≤
     subst (ind_subst mdecl ind u') #|Γ| (subst_instance u' t)).
Proof.
  intros decli cu ru cl cum pos.
  pose proof (proj1 decli) as declm.
  induction pos.
  - rewrite -(app_context_nil_l (_ ,,, _)) app_context_assoc in cum.
    eapply substitution_ws_cumul_pb in cum; eauto.
    2:{ eapply subslet_inds; eauto. }
    rewrite !subst_closedn ?closedn_subst_instance //.
    rewrite !subst_closedn ?closedn_subst_instance // in cum; len; auto.
    now rewrite app_context_nil_l in cum.

  - epose proof (ws_cumul_pb_is_closed_context cum).
    rewrite !subst_instance_mkApps !subst_mkApps in cum |- ×.
    simpl in cum. eapply ws_cumul_pb_mkApps_tRel in cum; eauto; cycle 1.
    { rewrite nth_error_app_ge // subst_instance_length //
         nth_error_subst_instance.
      unfold ind_arities, arities_context.
      rewrite rev_map_spec -map_rev.
      rewrite nth_error_map e /=. reflexivity. }
    1:trivial.
    rewrite -(app_context_nil_l (_ ,,, _)) app_context_assoc in cum.
    eapply ws_cumul_pb_terms_subst in cum.
    3:{ eapply subslet_untyped_subslet, (subslet_inds (u:=u)); eauto. }
    3:{ eapply subslet_untyped_subslet, (subslet_inds (u:=u)); eauto. }
    2:{ rewrite app_context_nil_l; eauto with fvs.
        move: H. rewrite on_free_vars_ctx_app ⇒ /andP[] //. }
    2:{ pose proof (inds_is_open_terms [] ind mdecl u).
        solve_all. eapply All_All2; tea.
        cbn; intros. eapply ws_cumul_pb_refl; eauto. }
    rewrite app_context_nil_l // in cum. len in cum.
    rewrite /ind_subst.
    eapply ws_cumul_pb_mkApps_eq ⇒ //.
    × move: cl. rewrite -is_closed_ctx_closed ⇒ cl.
      apply (closedn_ctx_subst 0 0). cbn. len.
      rewrite !closedn_subst_instance_context. rewrite /ind_arities in cl.
      move: cl. rewrite closedn_subst_instance_context closedn_ctx_app. len. move/andP⇒ []//.
      eapply closed_inds.
    × cbn. destruct (leb_spec_Set #|ctx| k); try lia.
      destruct (nth_error (inds _ _ _) _) eqn:hnth.
      eapply inds_nth_error in hnth as [n ->]. now cbn.
      eapply nth_error_None in hnth. len in hnth; lia.
    × cbn. destruct (leb_spec_Set #|ctx| k); try lia.
      destruct (nth_error (inds _ _ _) _) eqn:hnth.
      eapply inds_nth_error in hnth as [n ->]. now cbn.
      eapply nth_error_None in hnth. len in hnth; lia.
    × rewrite !map_length.
      simpl. destruct (Nat.leb #|ctx| k) eqn:eqle.
      eapply Nat.leb_le in eqle.
      rewrite /ind_subst !inds_spec !rev_mapi !nth_error_mapi.
      rewrite e /=. simpl. constructor. simpl.
      unfold R_global_instance. simpl.
      assert(declared_inductive Σ {|
      inductive_mind := inductive_mind ind;
      inductive_ind := Nat.pred #|ind_bodies mdecl| - (k - #|ctx|) |} mdecl i).
      { split; auto. simpl. rewrite -e nth_error_rev; lia_f_equal. }
      rewrite (declared_inductive_lookup H0) //.
      destruct (on_declared_inductive H0) as [onmind onind] ⇒ //. simpl in ×.
      rewrite e0 /ind_realargs.
      rewrite !onind.(ind_arity_eq).
      rewrite !destArity_it_mkProd_or_LetIn /=; len; simpl.
      rewrite (Nat.leb_refl) //. eapply Nat.leb_nle in eqle. lia.
    × do 2 eapply All2_map. do 2 eapply All2_map_inv in cum.
      eapply All2_All in cum. apply All_All2_refl.
      solve_all.
      now rewrite !subst_closedn ?closedn_subst_instance // in b |- ×.

  - simpl. simpl in cum.
    eapply ws_cumul_pb_LetIn_subst. eauto.
    { rewrite -(app_context_nil_l (_ ,,, _)) app_context_assoc in cum.
      eapply substitution_ws_cumul_pb in cum.
      2:{ eapply (subslet_inds (u:=u)); eauto. }
      rewrite app_context_nil_l /= in cum.
      rewrite /ind_subst. eapply ws_cumul_pb_is_open_term_left in cum.
      now rewrite subst_instance_length in cum. }
    { eapply ws_cumul_pb_is_open_term_right in cum.
    { rewrite -(app_context_nil_l (_ ,,, _)) app_context_assoc in cum.
      eapply is_open_term_subst_gen in cum.
      2:{ rewrite // app_context_nil_l //.
          rewrite - !is_closed_ctx_closed.
          now rewrite subst_instance_app_ctx in cl. }
          
      { cbn -[PCUICOnFreeVars.on_free_vars] in cum.
        rewrite subst_instance_length app_context_nil_l in cum. eapply cum. }
      1-2:eapply inds_is_open_terms. len. len. } }
    rewrite !subst_instance_subst /= in IHpos.
    rewrite !distr_subst /= in IHpos. rewrite /subst1.
    eapply IHpos ⇒ //.
    eapply ws_cumul_pb_LetIn_inv in cum; eauto.

  - simpl in cum |- ×.
    eapply ws_cumul_pb_Prod_Prod_inv_l in cum as [eqna dom codom]; eauto.
    eapply ws_cumul_pb_Prod; eauto.
    × rewrite -(app_context_nil_l (_ ,,, _)) app_context_assoc in dom.
      eapply substitution_ws_cumul_pb in dom; rewrite ?app_context_nil_l; eauto.
      2:{ eapply subslet_inds; eauto. }
      rewrite ?app_context_nil_l ?closedn_subst_instance // in dom.
      rewrite !subst_closedn ?closedn_subst_instance // in dom; len; auto.
      now rewrite !subst_closedn ?closedn_subst_instance.
    × cbn -[closedn_ctx] in IHpos. rewrite subst_context_snoc in IHpos.
      rewrite map_length Nat.add_0_r in IHpos. eapply IHpos; eauto.
      cbn. rewrite cl /=. len.
      rewrite closedn_subst_instance.
      eapply closed_upwards; eauto; lia.
Qed.

Lemma positive_cstr_closed_args_subst_arities {cf} {Σ} {wfΣ : wf Σ} {u u' Γ}
   {i ind mdecl idecl cdecl ind_indices cs} :
  declared_inductive Σ ind mdecl idecl →
  consistent_instance_ext Σ (ind_universes mdecl) u →
  on_constructor cumulSpec0 (lift_typing typing) (Σ.1, ind_universes mdecl) mdecl i idecl ind_indices cdecl cs →
  R_opt_variance (eq_universe Σ) (leq_universe Σ) (ind_variance mdecl) u u' →
  closed_ctx (subst_instance u (ind_params mdecl)) →
  wf_local Σ (subst_instance u (ind_arities mdecl ,,, smash_context [] (ind_params mdecl) ,,, Γ)) →
  All_local_env
    (fun (Γ : PCUICEnvironment.context) (t : term) (_ : typ_or_sort) ⇒
           positive_cstr_arg mdecl ([] ,,, (smash_context [] (ind_params mdecl) ,,, Γ)) t)
      Γ →
  assumption_context Γ →
  ws_cumul_ctx_pb_rel Cumul Σ (subst_instance u (ind_arities mdecl) ,,,
      subst_instance u
        (smash_context [] (PCUICEnvironment.ind_params mdecl)))
   (subst_instance u Γ) (subst_instance u' Γ) →
  ws_cumul_ctx_pb_rel Cumul Σ (subst_instance u (smash_context [] (PCUICEnvironment.ind_params mdecl)))
    (subst_context (ind_subst mdecl ind u) (context_assumptions (ind_params mdecl)) (subst_instance u Γ))
    (subst_context (ind_subst mdecl ind u') (context_assumptions (ind_params mdecl)) (subst_instance u' Γ)).
Proof.
  intros × decli cu onc onv cl wf cpos ass.
  intros [clΓ cum].
  split.
  rewrite -is_closed_ctx_closed.
  rewrite subst_instance_smash.
  now apply closedn_smash_context.
  revert cum.
  induction cpos; simpl; rewrite ?subst_context_nil ?subst_context_snoc; try solve [constructor; auto].
  all:rewrite ?map_length; intros cv; depelim cv; depelim wf.
  assert (isType Σ
  (subst_instance u (ind_arities mdecl) ,,,
   subst_instance u (smash_context [] (ind_params mdecl) ,,, Γ))
  (subst_instance u t)).
  { rewrite -subst_instance_app_ctx.
    destruct l as [s Hs]. ∃ s.
    move: Hs. cbn.
    now rewrite app_context_assoc. }
  depelim a.
  all:constructor.
  - eapply IHcpos. auto. now depelim ass. apply cv.
  - constructor; auto. cbn in ×.
    eapply positive_cstr_arg_subst in t0; eauto. len.
    move: t0.
    rewrite app_context_nil_l subst_instance_app_ctx subst_context_app.
    rewrite closed_ctx_subst //.
    rewrite subst_instance_smash.
    now apply closedn_smash_context.
    len.
    rewrite app_context_nil_l !subst_instance_app_ctx // app_context_assoc //.
    eapply ws_cumul_pb_is_closed_context in eqt.
    now rewrite is_closed_ctx_closed.
    rewrite app_context_nil_l !subst_instance_app_ctx // app_context_assoc //.
  - elimtype False; now depelim ass.
  - elimtype False; now depelim ass.
Qed.

Lemma positive_cstr_closed_args {cf} {Σ} {wfΣ : wf Σ} {u u'}
  {ind mdecl idecl cdecl} :
  declared_constructor Σ ind mdecl idecl cdecl →
  consistent_instance_ext Σ (ind_universes mdecl) u →
  R_opt_variance (eq_universe Σ) (leq_universe Σ) (ind_variance mdecl) u u' →
 ws_cumul_ctx_pb_rel Cumul Σ (subst_instance u (ind_arities mdecl) ,,,
    subst_instance u
      (smash_context [] (PCUICEnvironment.ind_params mdecl)))
 (smash_context []
    (subst_instance u
       (expand_lets_ctx (PCUICEnvironment.ind_params mdecl)
          (cstr_args cdecl))))
 (smash_context []
    (subst_instance u'
       (expand_lets_ctx (PCUICEnvironment.ind_params mdecl)
          (cstr_args cdecl)))) →

  ws_cumul_ctx_pb_rel Cumul Σ (subst_instance u (smash_context [] (PCUICEnvironment.ind_params mdecl)))
      (subst_context (inds (inductive_mind ind.1) u (ind_bodies mdecl)) (context_assumptions (ind_params mdecl))
       (smash_context []
          (subst_instance u
             (expand_lets_ctx (PCUICEnvironment.ind_params mdecl)
                (cstr_args cdecl)))))
       (subst_context (inds (inductive_mind ind.1) u' (ind_bodies mdecl)) (context_assumptions (ind_params mdecl))
           ((smash_context []
          (subst_instance u'
             (expand_lets_ctx (PCUICEnvironment.ind_params mdecl)
                (cstr_args cdecl)))))).
Proof.
  intros × declc cu Ru cx.
  pose proof (on_declared_constructor declc) as [[onmind oib] [cs [? onc]]].
  pose proof (onc.(on_ctype_positive)) as cpos.
  rewrite onc.(cstr_eq) in cpos. unf_env.
  rewrite -it_mkProd_or_LetIn_app in cpos.
  eapply positive_cstr_it_mkProd_or_LetIn in cpos as [hpars _].
  rewrite smash_context_app_expand in hpars.
  eapply All_local_env_app_inv in hpars as [_hpars hargs].
  rewrite expand_lets_smash_context /= expand_lets_k_ctx_nil /= in hargs.
  eapply positive_cstr_closed_args_subst_arities in hargs; eauto.
  split.
  - rewrite !subst_instance_smash /ind_subst /= in hargs |- ×.
    eapply hargs; eauto.
  - destruct hargs as [hargs hwf]. now rewrite !subst_instance_smash in hwf |- ×.
  - eapply declc.
  - eapply closed_wf_local; eauto; eapply on_minductive_wf_params; eauto; eapply declc.
  - rewrite -app_context_assoc. rewrite -(expand_lets_smash_context _ []).
    rewrite -smash_context_app_expand subst_instance_app_ctx subst_instance_smash.
    eapply wf_local_smash_end; eauto.
    rewrite -subst_instance_app_ctx app_context_assoc.
    now epose proof (on_constructor_inst declc _ cu) as [wfarpars _].
  - eapply smash_context_assumption_context. constructor.
  - now rewrite !(subst_instance_smash _ (expand_lets_ctx _ _)).
Qed.

Lemma red_subst_instance {cf:checker_flags} (Σ : global_env) (Γ : context) (u : Instance.t) (s t : term) :
  red Σ Γ s t →
  red Σ (subst_instance u Γ) (subst_instance u s)
            (subst_instance u t).
Proof.
  intros H; apply clos_rt_rt1n in H.
  apply clos_rt1n_rt.
  induction H. constructor.
  eapply red1_subst_instance in r.
  econstructor 2. eapply r. auto.
Qed.

Lemma assumption_context_map f Γ :
  assumption_context Γ → assumption_context (map_context f Γ).
Proof.
  induction 1; constructor; auto.
Qed.

Lemma assumption_context_subst_instance u Γ :
  assumption_context Γ → assumption_context (subst_instance u Γ).
Proof. apply assumption_context_map. Qed.

Section Betweenu.
  Context (start : nat) (k : nat).

  Definition betweenu_level (l : Level.t) :=
    match l with
    | Level.Var n ⇒ (start <=? n) && (n <? start + k)%nat
    | _ ⇒ true
    end.

  Definition betweenu_level_expr (s : LevelExpr.t) :=
    betweenu_level (LevelExpr.get_level s).

  Definition betweenu_universe0 (u : LevelAlgExpr.t) :=
    LevelExprSet.for_all betweenu_level_expr u.

  Definition betweenu_universe (u : Universe.t) :=
    match u with
    | Universe.lProp | Universe.lSProp ⇒ true
    | Universe.lType l ⇒ betweenu_universe0 l
    end.

  Definition betweenu_instance (u : Instance.t) :=
    forallb betweenu_level u.

End Betweenu.