Library MetaCoq.Erasure.ErasureCorrectness

Correctness of erasure


Notation "Σ |-p s ▷ t" := (eval Σ s t) (at level 50, s, t at next level) : type_scope.
Notation "Σ ⊢ s ▷ t" := (EWcbvEval.eval Σ s t) (at level 50, s, t at next level) : type_scope.

The correctness proof


#[export] Hint Constructors PCUICWcbvEval.eval erases : core.

Import ssrbool.

Lemma erases_correct (wfl := default_wcbv_flags) Σ t T t' v Σ' :
  wf_ext Σ
  Σ;;; [] |- t : T
  Σ;;; [] |- t t'
  erases_deps Σ Σ' t'
  Σ |-p t v
   v', Σ;;; [] |- v v' Σ' t' v' .
Proof.
  intros wfΣ Hty He Hed H.
  revert T Hty t' He Hed.
  induction H; intros T Hty t' He Hed.
  - assert (Hty' := Hty).
    assert (eval Σ (PCUICAst.tApp f a) res) by eauto.
    eapply inversion_App in Hty as (? & ? & ? & ? & ? & ?).
    invs He.

    + depelim Hed.
      eapply IHeval1 in H4 as (vf' & Hvf' & [He_vf']); eauto.
      eapply IHeval2 in H6 as (vu' & Hvu' & [He_vu']); eauto.
      pose proof (subject_reduction_eval t0 H).
      eapply inversion_Lambda in X0 as (? & ? & ? & ? & e0).
      assert (Σ ;;; [] |- a' : t). {
          eapply subject_reduction_eval; eauto.
          eapply PCUICConversion.ws_cumul_pb_Prod_Prod_inv in e0 as [? e1 e2].
          eapply type_Cumul_alt. eassumption. now x2.
          symmetry in e1.
          eapply ws_cumul_pb_forget in e1.
          now eapply conv_cumul. }
      assert (eqs := type_closed_subst b wfΣ X0).
      invs Hvf'.
      × assert (Σ;;; [] |- PCUICAst.subst1 a' 0 b ELiftSubst.subst1 vu' 0 t').
        eapply (erases_subst Σ [] [vass na t] [] b [a'] t'); eauto.
        econstructor. econstructor. rewrite PCUICLiftSubst.subst_empty. eassumption.
        rewrite eqs in H2.
        eapply IHeval3 in H2 as (v' & Hv' & [He_v']).
        -- v'. split; eauto.
           constructor.
           econstructor; eauto.
           rewrite ECSubst.closed_subst; auto.
           eapply erases_closed in Hvu'; auto; fvs.
        -- rewrite <-eqs. eapply substitution0; eauto.
        -- eapply erases_deps_subst1; [now eauto|].
           eapply erases_deps_eval in He_vf'; [|now eauto].
           depelim He_vf'.
           assumption.
      × EAst.tBox. split.
        eapply Is_type_lambda in X1; eauto. destruct X1. econstructor.
        eapply (is_type_subst Σ [] [vass na _] [] _ [a']) in X1 ; auto.
        cbn in X1.
        eapply Is_type_eval; try assumption.
        eauto. eapply H1. rewrite <-eqs. eassumption.
        all: eauto. econstructor. econstructor. rewrite PCUICLiftSubst.subst_empty.
        eauto. constructor. econstructor. eauto. eauto.
      × auto.
    + EAst.tBox. split. 2:constructor; econstructor; eauto.
      econstructor.
      eapply Is_type_eval; eauto.
    + auto.
  - assert (Hty' := Hty).
    assert (Σ |-p tLetIn na b0 t b1 res) by eauto.
    eapply inversion_LetIn in Hty' as (? & ? & ? & ? & ? & ?); auto.
    invs He.
    + depelim Hed.
      eapply IHeval1 in H6 as (vt1' & Hvt2' & [He_vt1']); eauto.
      assert (Hc : conv_context cumulAlgo_gen Σ ([],, vdef na b0 t) [vdef na b0' t]). {
        econstructor. econstructor. econstructor. reflexivity.
        eapply PCUICCumulativity.red_conv.
        now eapply wcbeval_red; eauto.
        reflexivity.
      }
      assert (Σ;;; [vdef na b0' t] |- b1 : x0). {
        cbn in ×. eapply context_conversion. 3:eauto. all:cbn; eauto.
        econstructor. all: hnf; eauto. eapply subject_reduction_eval; auto. eauto. eauto.
      }
      assert (Σ;;; [] |- subst1 b0' 0 b1 ELiftSubst.subst1 vt1' 0 t2'). {
        eapply (erases_subst Σ [] [vdef na b0' t] [] b1 [b0'] t2'); eauto.
        enough (subslet Σ [] [subst [] 0 b0'] [vdef na b0' t]).
        now rewrite PCUICLiftSubst.subst_empty in X1.
        econstructor. econstructor.
        rewrite !PCUICLiftSubst.subst_empty.
        eapply subject_reduction_eval; eauto.
        eapply erases_context_conversion. 3:eassumption.
        all: cbn; eauto.
        econstructor. all: hnf; eauto.
        eapply subject_reduction_eval; eauto.
      }
      pose proof (subject_reduction_eval t1 H).
      assert (eqs := type_closed_subst b1 _ X1).
      rewrite eqs in H1.
      eapply IHeval2 in H1 as (vres & Hvres & [Hty_vres]); [| |now eauto].
      2:{ rewrite <-eqs. eapply substitution_let; eauto. }
       vres. split. eauto. constructor; econstructor; eauto.
      enough (ECSubst.csubst vt1' 0 t2' = ELiftSubst.subst10 vt1' t2') as ->; auto.
      eapply ECSubst.closed_subst. eapply erases_closed in Hvt2'; auto.
      eapply eval_closed. eauto. 2:eauto. now eapply subject_closed in t1.
    + EAst.tBox. split. 2:constructor; econstructor; eauto.
      econstructor. eapply Is_type_eval; eauto.

  - assert (Σ |-p tConst c u res) by eauto.
    eapply inversion_Const in Hty as (? & ? & ? & ? & ?); [|easy].
    invs He.
    + depelim Hed.
      assert (isdecl' := isdecl).
      eapply declared_constant_inj in H0; [|now eauto]; subst.
      unfold erases_constant_body in ×. rewritee in ×.
      destruct ?; try tauto. cbn in ×.
      eapply declared_constant_inj in d; [|now eauto]; subst.
      edestruct IHeval as (? & ? & [?]).
      × cbn in ×.
        assert (isdecl'' := isdecl').
        eapply declared_constant_inv in isdecl'; [| |now eauto|now apply wfΣ].
        2:eapply weaken_env_prop_typing.
        unfold on_constant_decl in isdecl'. rewrite e in isdecl'. red in isdecl'.
        unfold declared_constant in isdecl''.
        now eapply @typing_subst_instance_decl with (Σ := Σ) (Γ := []); eauto.
      × assert (isdecl'' := isdecl').
        eapply declared_constant_inv in isdecl'; [| |now eauto|now apply wfΣ].
        unfold on_constant_decl in isdecl'. rewrite e in isdecl'. cbn in ×.
        2:eapply weaken_env_prop_typing.
        now eapply erases_subst_instance_decl with (Σ := Σ) (Γ := []); eauto.
      × now eauto.
      × x0. split; eauto. constructor; econstructor; eauto.
    + EAst.tBox. split. econstructor.
      eapply Is_type_eval. 3: eassumption. eauto. eauto. eauto. constructor. econstructor. eauto.

  - assert (Hty' := Hty).
  assert (Σ |-p tCase ci p discr brs res) by eauto.
  eapply inversion_Case in Hty' as (mdecl' & idecl' & di & indices & [] & c0); auto.

  rename ci into ind.
  pose proof d as d'. eapply declared_constructor_inductive in d'.
  edestruct (declared_inductive_inj d' di); subst. clear d'.

  assert (Σ ;;; [] |- mkApps (tConstruct ind c u) args : mkApps (tInd ind (puinst p)) (pparams p ++ indices)).
  eapply subject_reduction_eval; eauto.
  assert (Hcstr := X0).
  eapply Construct_Ind_ind_eq in X0; tea. 2:pcuic.
  destruct X0 as (((([_ Ru] & cu) & cpu) & ?) & (parsubst & argsubst & parsubst' & argsubst' & [])).
  invs He.
  + depelim Hed.
    rename H1 into decli. rename H2 into decli'.
    rename H3 into em. rename Hed into er.
    edestruct (IHeval1 _ scrut_ty) as (v' & Hv' & [He_v']); eauto.
    pose proof e as Hnth.
    assert (lenppars : ind_npars mdecl = #|pparams p|).
    { now rewrite (wf_predicate_length_pars wf_pred). }
    destruct (declared_inductive_inj d decli); subst mdecl0 idecl0.
    eapply erases_mkApps_inv in Hv' as [(? & ? & ? & ? & [] & ? & ? & ?) | (? & ? & ? & ? & ?)]; eauto.
    × subst.
      eapply Is_type_app in X1; auto. destruct X1.
      2:{ rewrite -mkApps_app; tea. }
      rewrite -mkApps_app in X1.

      eapply tConstruct_no_Type in X1; auto.

      eapply H6 in X1 as []; eauto. 2: split; auto; []; now destruct Σ.

      destruct (ind_ctors idecl) eqn:hctors.
      { cbn in ×. depelim brs_ty. rewrite nth_error_nil // in Hnth. }
      depelim brs_ty. cbn in H1.
      destruct l; cbn in *; try lia.
      depelim brs_ty. depelim X0. depelim X0.
      destruct p1.
      destruct c; cbn in ×. noconf Hnth. 2:{ rewrite nth_error_nil // in Hnth. }
      destruct p0 as (? & ? & ? & ?).
      assert (c1 = cdecl).
      { destruct d. rewrite hctors /= in H10. now noconf H10. }
      depelim H5.
      subst c1.
      destruct y0 as [n br']; cbn in ×.
      rename y into br.
      edestruct IHeval2 as (? & ? & [?]).
      eapply subject_reduction. eauto. exact Hty.
      etransitivity.
      eapply PCUICReduction.red_case_c. eapply wcbeval_red; eauto.
      econstructor. econstructor.
      eauto.
      all:unfold iota_red in ×. all:cbn in ×.
      { rewrite e3 e1. now f_equal. }
      {
        assert (expand_lets (inst_case_branch_context p br) (br.(PCUICAst.bbody)) = br.(PCUICAst.bbody)) as →. {
          unshelve edestruct @on_declared_constructor as (? & ? & ? & []). 8: exact d. all: eauto.
          pattern br.
          eapply All_nth_error.
          eapply (expand_lets_erasure (p:=p) d wf_brs); eauto.
          rewrite hctors; constructor.
          solve_all. constructor.
          instantiate (1 := 0); cbn; eassumption.
        }
        invs H9.
        eapply erases_subst0; eauto.
        rewrite [case_branch_context_gen _ _ _ _ _ _]PCUICCasesContexts.inst_case_branch_context_eq; eauto.
        1:{ unfold app_context. cbn. rewrite app_nil_r.
            eapply (subslet_cstr_branch_context (u:=u)); tea.
            - rewrite lenppars firstn_app_left // in s0. exact s0.
            - eapply (declared_constructor_assumption_context d).
            - destruct s3 as [Hs [_ []]].
              rewrite {2}lenppars [firstn _ (pparams p ++ _)]firstn_app_left // in a1.
            - red in wf_brs. rewrite hctors in wf_brs. now depelim wf_brs.
            - rewrite -eq_npars. exact s1. }
        eapply All2_rev.
        rewrite -eq_npars.
        eapply All_All2_flex; tea.
        2:{ instantiate (1 := repeat EAst.tBox #|skipn (ind_npars mdecl) (x ++ x0)|).
            now rewrite repeat_length. }
        intros ? ? ? % repeat_spec. subst.
        constructor.
        now eapply isErasable_Proof. }
      2:{
       x2. split; eauto. constructor. eapply eval_iota_sing ⇒ //.
      pose proof (Ee.eval_to_value _ _ He_v').
      eapply value_app_inv in X0. subst. eassumption.
      depelim H2.
      eapply isErasable_Propositional in X0; eauto.
      rewrite -eq_npars.
      eapply isPropositional_propositional; eauto.
      invs e. cbn in ×.
      rewrite map_length.
      rewrite skipn_length e3 e2 in H11.
      rewrite (@assumption_context_assumptions (bcontext br)) // ?rev_repeat in H11 ⇒ //.
      { eapply assumption_context_compare_decls. symmetry in a. exact a.
        rewrite /cstr_branch_context. eapply assumption_context_expand_lets_ctx.
        eapply assumption_context_subst_context.
        apply (declared_constructor_assumption_context d). }
      rewrite ECSubst.substl_subst //.
      { eapply forallb_repeat. econstructor. }
      replace (ind_npars mdecl + #|bcontext br| - ind_npars mdecl)
      with #|bcontext br| in H11 by lia. eauto.
      }
      depelim H4.
      cbn in H1.
      eapply erases_deps_subst. 2: eauto.
      eapply All_rev. eapply Forall_All.
      eapply All_Forall, All_repeat. econstructor.
    × subst. unfold iota_red in ×.
      destruct (All2_nth_error_Some _ _ X0 Hnth) as (? & ? & ? & ?).
      destruct (All2i_nth_error_r _ _ _ _ _ _ brs_ty Hnth) as (? & ? & ? & ? & ? & ?).
      cbn in ×. subst.
      assert (declared_constructor Σ (ind, c) mdecl idecl x2).
      { split; tea. }
      destruct (declared_constructor_inj d H1) as [_ [_ <-]]. clear H1.
      edestruct IHeval2 as (? & ? & [?]).
      eapply subject_reduction. eauto. exact Hty.
      etransitivity.
      eapply PCUICReduction.red_case_c. eapply wcbeval_red. eauto.
      eauto. eauto.

      etransitivity. constructor. constructor.
      eauto.
      { rewrite e0 /cstr_arity e2 e1 //. }
      unfold iota_red. reflexivity.

      {
        assert (expand_lets (inst_case_branch_context p br) (br.(PCUICAst.bbody)) = br.(PCUICAst.bbody)) as →. {
        unshelve edestruct @on_declared_constructor as (? & ? & ? & []). 8: exact d. all: eauto.
          pattern br.
          eapply All_nth_error. 2: eauto.
          eapply (expand_lets_erasure d wf_brs). solve_all.
        }
        eapply erases_subst0; eauto.
        all: try rewrite case_branch_type_fst PCUICCasesContexts.inst_case_branch_context_eq; eauto.
        rewrite app_context_nil_l.
        erewrite <-PCUICCasesContexts.inst_case_branch_context_eq; eauto.
        1:{ eapply (subslet_cstr_branch_context (u:=u)); tea.
            - rewrite lenppars firstn_app_left // in s0. exact s0.
            - eapply (declared_constructor_assumption_context d).
            - destruct s3 as [Hs [_ []]].
              rewrite {2}lenppars [firstn _ (pparams p ++ _)]firstn_app_left // in a1.
            - red in wf_brs. eapply Forall2_All2 in wf_brs.
              eapply All2_nth_error in wf_brs; tea.
            - rewrite -eq_npars. exact s1. }
      eapply All2_rev. eapply All2_skipn.
      eapply Forall2_All2 in H3. eapply All2_impl. exact H3. intros. eauto.
       }
      
      eapply nth_error_forall in H5; [|now eauto].
      eapply erases_deps_subst; eauto.
      eapply All_rev.
      eapply erases_deps_eval in He_v'; [|now eauto].
      eapply erases_deps_mkApps_inv in He_v' as (? & ?).
      now eapply All_skipn, Forall_All.

      invs H2.
      -- x2. split; eauto.
         constructor. econstructor. eauto. eauto. 2:eauto.
         4:{ unfold EGlobalEnv.iota_red.
          rewrite ECSubst.substl_subst //.
          rewrite forallb_rev forallb_skipn //.
          assert (forallb (closedn 0) args).
          { move/eval_closed: H; tea.
            move/(_ (subject_closed scrut_ty)).
            now rewrite closedn_mkApps /=. }
          solve_all. eapply (erases_closed _ []); tea. }
         rewrite -eq_npars.
         eapply isPropositional_propositional_cstr; eauto.
         rewrite -(Forall2_length H3) /= e1 //.
         rewrite skipn_length -(Forall2_length H3) -e6 /= map_length.
         rewrite (All2_length a).
         replace #|cstr_branch_context ind mdecl cdecl|
          with (context_assumptions (cstr_branch_context ind mdecl cdecl)).
         2:{ eapply assumption_context_assumptions.
             eapply (assumption_context_cstr_branch_context d). }
         rewrite e0 /cstr_arity e1 cstr_branch_context_assumptions; lia.
      -- eapply Is_type_app in X1 as []; auto.
         2:{ eapply subject_reduction_eval. 2:eassumption. eauto. }
         assert (ispind : inductive_isprop_and_pars Σ' ind = Some (true, ind_npars mdecl)).
         { eapply isPropositional_propositional; eauto. eapply isErasable_Propositional; eauto. }

         eapply tConstruct_no_Type in X1; auto.
         eapply H6 in X1 as []; eauto. 2:reflexivity.

         destruct (ind_ctors idecl) eqn:hctors. cbn in ×. destruct c; invs e7.
         destruct l; cbn in *; try lia. destruct c as [ | []]; cbn in *; invs e7.

         destruct brs'; invs e4.
         destruct brs; invs Hnth.
         destruct H9.
         depelim brs_ty. depelim brs_ty.
         depelim X0. depelim X0.
         destruct p0 as (? & ? & ? & ?).
         edestruct IHeval2 as (? & ? & [?]).
         eapply subject_reduction. eauto. exact Hty.
         etransitivity.
         eapply PCUICReduction.red_case_c. eapply wcbeval_red. eauto.
         eauto. eauto.
         etransitivity. constructor. constructor. cbn. reflexivity.
         { rewrite e0 /cstr_arity e2 e1 //. }
         eauto.

         {
          assert (expand_lets (inst_case_branch_context p br) (br.(PCUICAst.bbody)) = br.(PCUICAst.bbody)) as →. {
            unshelve edestruct @on_declared_constructor as (? & ? & ? & []). 8: exact d. all: eauto.
            pattern br.
            eapply All_nth_error.
            eapply expand_lets_erasure; eauto.
            2: instantiate (1 := 0); cbn; eassumption.
            rewrite hctors. constructor; auto. constructor. }
          destruct p1.
          eapply erases_subst0; eauto.
          - rewrite case_branch_type_fst PCUICCasesContexts.inst_case_branch_context_eq; eauto.
          - rewrite app_context_nil_l.
            eapply subslet_cstr_branch_context. tea. exact cu. all:eauto.
            now rewrite lenppars firstn_app_left // in s0.
            eapply (declared_constructor_assumption_context d).
            destruct s3 as [? [? [eqp _]]].
            rewrite lenppars (firstn_app_left) // in eqp. congruence.
            move: wf_brs. now rewrite /wf_branches hctorsh; depelim h.
            rewrite -eq_npars. exact s1.
          - eapply All2_rev. cbn.
            rewrite -eq_npars.
            eapply All_All2_flex.
            exact X1.
            intros ? ? → % repeat_spec.
            intros. econstructor. eapply isErasable_Proof. eauto.
            rewrite repeat_length. reflexivity.
        }

         depelim H5.
         eapply erases_deps_subst; eauto.
         eapply All_rev, All_repeat.
         econstructor.

          x. split; eauto.
         constructor.
         destruct x1 as [n br'].
         eapply eval_iota_sing ⇒ //.
         pose proof (Ee.eval_to_value _ _ He_v').
         apply value_app_inv in X0; subst x0.
         apply He_v'.
         now rewrite -eq_npars.

         cbn in ×.

         rewrite ECSubst.substl_subst.
         { eapply forallb_repeat. econstructor. }

         rewrite rev_repeat in H10.

         enough (#|skipn (ind_npars mdecl) args| = #|n|) as <- by eauto.
         edestruct invert_Case_Construct as (? & ? & ? & ?).
         { econstructor. eauto. }
         { eapply subject_reduction. eauto. exact Hty.
           eapply PCUICReduction.red_case_c. eapply wcbeval_red; eauto. }

        rewrite eq_npars. rewrite List.skipn_length e0 /cstr_arity -e1 e2.
        replace (ci_npar ind + context_assumptions (bcontext br) - ci_npar ind)
    with (context_assumptions (bcontext br)) by lia.
        subst n. rewrite map_length.
        rewrite assumption_context_assumptions //.
        eapply assumption_context_compare_decls. symmetry; tea.
        eapply (assumption_context_cstr_branch_context d).
    + EAst.tBox. split. econstructor.
      eapply Is_type_eval; eauto. constructor. econstructor; eauto.
  - pose (Hty' := Hty).
    pose proof (proj2 (proj2 d)) as eqpars.
    rename e0 into hnth. rename e into eargs.
    eapply inversion_Proj in Hty' as (? & ? & ? & [] & ? & ? & ? & ? & ? & ?); [|easy].
    assert (Hpars : p.(proj_npars) = ind_npars x0).
    { destruct (declared_constructor_inj d0 d). now subst. }
    invs He.

    + depelim Hed.
      rename H1 into decli. rename H2 into decli'. rename H4 into er. rename H3 into em. rename H5 into H3.
      eapply IHeval1 in H6 as (vc' & Hvc' & [Hty_vc']); eauto.
      eapply erases_mkApps_inv in Hvc'; eauto.
      destruct Hvc' as [ (? & ? & ? & ? & [] & ? & ? & ?) | (? & ? & ? & ? & ?)]; subst.
      × EAst.tBox.
        destruct (declared_inductive_inj decli d) as [<- <-].
        assert (isprop : inductive_isprop_and_pars Σ' p.(proj_ind) = Some (true, ind_npars mdecl)).
        { eapply isPropositional_propositional. exact d. all:eauto. apply decli'.
          eapply isErasable_Propositional; eauto. }
        split.
        eapply Is_type_app in X as []; eauto. 2:{ rewrite -mkApps_app. eapply subject_reduction_eval; eauto. }
        rewrite -mkApps_app in X.

        eapply tConstruct_no_Type in X; eauto. eapply H3 in X as [? []]; eauto.
        2:{ exact d. }
        2: split; auto; now []; destruct Σ.
        destruct d0 as (? & ? & ?).

        econstructor.
        eapply Is_type_eval; eauto.
        eapply nth_error_all.
        erewrite nth_error_skipn. eassumption.
        eapply All_impl.
        subst. rewrite -eqpars.
        eassumption.
        eapply isErasable_Proof. constructor. eauto.

        eapply eval_proj_prop ⇒ //.
        pose proof (Ee.eval_to_value _ _ Hty_vc').
        eapply value_app_inv in X0. subst. eassumption.
        now rewrite -eqpars.
      × rename H3 into Hinf.
        assert (lenx5 := Forall2_length H4).
        eapply Forall2_nth_error_Some in H4 as (? & ? & ?); eauto.
        assert (Σ ;;; [] |- mkApps (tConstruct p.(proj_ind) 0 u) args : mkApps (tInd p.(proj_ind) x) x3).
        eapply subject_reduction_eval; eauto.
        eapply inversion_mkApps in X as (? & ? & ?); eauto.
        eapply Prelim.typing_spine_inv in t1 as []; eauto.
        eapply IHeval2 in H3 as (? & ? & [?]); eauto.
        destruct (declared_projection_inj decli d0) as [? [? []]].
        subst x0 x1 cdecl0 x2.
        destruct (declared_projection_inj d d0) as [? [? []]]; subst mdecl0 idecl0 pdecl0 cdecl.
        invs H2.
        -- x9. split; eauto. constructor.
            eapply Ee.eval_proj; eauto. rewrite -eqpars.
            eapply isPropositional_propositional_cstr; eauto.
            apply d0. cbn. eapply decli'. cbn. rewrite -lenx5 //.
            move: eargs. unfold PCUICWcbvEval.cstr_arity; cbn.
            now rewrite -eqpars.
        -- EAst.tBox.
          assert (isprop : inductive_isprop_and_pars Σ' p.(proj_ind) = Some (true, ind_npars mdecl)).
          { eapply isPropositional_propositional; eauto. apply d. apply decli'.
            eapply (isErasable_Propositional (args:=[])); eauto. }
          split.
          eapply Is_type_app in X as []; eauto. 2:{ eapply subject_reduction_eval; [|eauto]; eauto. }

          eapply tConstruct_no_Type in X. eapply Hinf in X as [? []]; eauto.
          2: now eapply d. 2:reflexivity. 2:eauto.
          econstructor.
          eapply Is_type_eval; eauto.
          eapply nth_error_all.
          erewrite nth_error_skipn. eassumption. rewrite -eqpars.
          eapply All_impl.
          eassumption.
          eapply isErasable_Proof.
          constructor. eapply eval_proj_prop ⇒ //.
          pose proof (Ee.eval_to_value _ _ Hty_vc').
          eapply value_app_inv in X0. subst. eassumption.
          now rewrite -eqpars.
        -- eapply erases_deps_eval in Hty_vc'; [|now eauto].
            eapply erases_deps_mkApps_inv in Hty_vc' as (? & ?).
            now eapply nth_error_forall in H1; eauto.
    + EAst.tBox. split. econstructor.
      eapply Is_type_eval. 3: eassumption. all:eauto. constructor. econstructor. eauto.
  - assert (Hty' := Hty).
    assert (Hunf := H).
    assert (Hcon := H0).
    eapply inversion_App in Hty' as (? & ? & ? & ? & ? & e0); eauto.
    assert (Ht := t).
    eapply subject_reduction in t. 2:auto. 2:eapply wcbeval_red; eauto.
    assert (HT := t).
    apply PCUICValidity.inversion_mkApps in HT as (? & ? & ?); auto.
    assert (Ht1 := t1).
    apply inversion_Fix in t1 as Hfix; auto.
    destruct Hfix as (? & ? & ? & ? & ? & ? & e1).
    unfold cunfold_fix in e. rewrite e2 in e. invs e.
    depelim He; first last.

    + EAst.tBox. split; [|now constructor; constructor].
      econstructor.
      eapply Is_type_eval. 3:eapply X. eauto.
      eapply eval_fix; eauto.
      rewrite /cunfold_fix e2 //. now rewrite H3.
    + depelim Hed.
      eapply IHeval1 in He1 as (er_stuck_v & er_stuck & [ev_stuck]); eauto.
      eapply IHeval2 in He2 as (er_argv & er_arg & [ev_arg]); eauto.
      eapply erases_mkApps_inv in er_stuck; eauto.
      destruct er_stuck as [(? & ? & ? & → & ? & ? & ? & ->)|
                            (? & ? & → & ? & ?)].
      { E.tBox.
        eapply eval_to_mkApps_tBox_inv in ev_stuck as ?; subst.
        cbn in ×.
        split; [|constructor; eauto].
        2:{ eapply (eval_box_apps _ _ [_]); eauto. }
        destruct H2.
        eapply (Is_type_app _ _ _ (x5 ++ [av])) in X as []; eauto; first last.
        - rewrite -mkApps_app app_assoc mkApps_snoc.
          eapply PCUICValidity.type_App'; eauto.
          eapply subject_reduction; eauto.
          eapply wcbeval_red; eauto.
        - eapply erases_box.
          eapply Is_type_eval; auto. 2:eauto.
          rewrite mkApps_app /=.
          eapply eval_fix.
          rewrite -mkApps_app. eapply value_final.
          eapply eval_to_value; eauto.
          eapply value_final, eval_to_value; eauto.
          rewrite /cunfold_fix e2 //. auto.
          now rewrite H3. auto. }

      invs H2.
      × assert (Hmfix' := X).
        eapply All2_nth_error_Some in X as (? & ? & ?); eauto.
        pose proof (closed_fix_substl_subst_eq (subject_closed t1) e2) as cls.
        destruct x3. cbn in ×. subst.

        enough (Σ;;; [] ,,, subst_context (fix_subst mfix) 0 []
                |- subst (fix_subst mfix) 0 dbody
                 ELiftSubst.subst (EGlobalEnv.fix_subst mfix') 0 (Extract.E.dbody x4)).
        destruct a2.

        clear e3. rename H into e3.
        -- cbn in e3. rename x5 into L.
           eapply (erases_mkApps _ _ _ _ (argsv ++ [av])) in H2; first last.
           { eapply Forall2_app.
             - exact H4.
             - eauto. }
           rewrite mkApps_app in H2.
           rewrite EAstUtils.mkApps_app in H2.
           cbn in ×. simpl in H2.
          rewrite cls in H2.
          eapply IHeval3 in H2 as (? & ? & [?]); cbn; eauto; cycle 1.
           { eapply subject_reduction. eauto. exact Hty.
             etransitivity.
             eapply PCUICReduction.red_app. eapply wcbeval_red; eauto.
             eapply wcbeval_red; eauto.
             rewrite <- !mkApps_snoc.
             eapply PCUICReduction.red1_red.
             eapply PCUICReduction.red_fix.
             rewrite closed_unfold_fix_cunfold_eq.
             now eapply subject_closed in t1.
             rewrite /cunfold_fix e2 /= //.
             pose proof (eval_to_value _ _ _ e3) as vfix.
             eapply PCUICWcbvEval.stuck_fix_value_args in vfix; eauto.
             2:{ rewrite /cunfold_fix e2 //. }
             simpl in vfix.
             subst. unfold is_constructor.
             rewrite nth_error_snoc. lia.
             assert(Σ ;;; [] |- mkApps (tFix mfix idx) (argsv ++ [av]) : subst [av] 0 x1).
             { rewrite mkApps_app. eapply PCUICValidity.type_App'; eauto.
               eapply subject_reduction_eval; eauto. }
             epose proof (fix_app_is_constructor (args:=argsv ++ [av]) X).
             rewrite /unfold_fix e2 in X0.
             specialize (X0 eq_refl). simpl in X0.
             rewrite nth_error_snoc in X0. auto. apply X0.
             eapply value_axiom_free, eval_to_value; eauto.
             eapply value_whnf; eauto.
             eapply eval_closed; eauto. now eapply subject_closed in t0.
             eapply eval_to_value; eauto. }
           
           { constructor.
             - eapply erases_deps_eval in ev_stuck; [|now eauto].
               eapply erases_deps_mkApps_inv in ev_stuck as (? & ?).
               apply erases_deps_mkApps; [|now eauto].
               depelim H.
               eapply nth_error_forall in H as H'; eauto.
               apply erases_deps_subst; [|now eauto].
               now apply Forall_All, Forall_erases_deps_fix_subst; eauto.
             - now eapply erases_deps_eval in ev_arg; eauto. }

            x3. split. eauto.
           constructor. eapply Ee.eval_fix.
           ++ eauto.
           ++ eauto.
           ++ eauto.
           ++ rewrite <- Ee.closed_unfold_fix_cunfold_eq.
              { unfold EGlobalEnv.unfold_fix. rewrite e -e4.
                now rewrite (Forall2_length H4). }
              eapply eval_closed in e3; eauto.
              clear -e3 Hmfix'.
              pose proof (All2_length Hmfix').
              rewrite closedn_mkApps in e3.
              apply andb_true_iff in e3 as (e3 & _).
              change (?a = true) with (is_true a) in e3.
              simpl in e3 |- ×. solve_all.
              rewrite app_context_nil_l in b.
              destruct b as [eqb eqrar isl isl' e].
              eapply erases_closed in e. simpl in e.
              rewrite <- H.
              unfold EAst.test_def.
              simpl in e.
              rewrite fix_context_length in e.
              now rewrite Nat.add_0_r.
              unfold test_def in a. apply andb_and in a as [_ Hbod].
              rewrite fix_context_length.
              now rewrite Nat.add_0_r in Hbod.
              eauto with pcuic.
              now eapply subject_closed in Ht.
          ++ auto.

        -- cbn. destruct a2 as [eqb eqrar isl isl' e5].
           eapply (erases_subst Σ [] (fix_context mfix) [] dbody (fix_subst mfix)) in e5; cbn; eauto.
           ++ eapply subslet_fix_subst. now eapply wf_ext_wf. all: eassumption.
           ++ eapply nth_error_all in a1; eauto. cbn in a1.
              eapply a1.
           ++ eapply All2_from_nth_error.
              erewrite fix_subst_length, EGlobalEnv.fix_subst_length, All2_length; eauto.
              intros.
              rewrite fix_subst_nth in H3. now rewrite fix_subst_length in H2.
              rewrite efix_subst_nth in H5. rewrite fix_subst_length in H2.
              erewrite <- All2_length; eauto.
              invs H5; invs H3.
              erewrite All2_length; eauto.
      × eapply (Is_type_app _ _ _ (argsv ++ [av])) in X as []; tas.
        -- EAst.tBox.
           split.
           ++ econstructor.
              eapply Is_type_eval. 3:eauto. all:eauto.
              rewrite mkApps_app.
              eapply eval_fix; eauto.
              1-2:eapply value_final, eval_to_value; eauto.
              rewrite /cunfold_fix e2 //. congruence.
           ++ constructor. eapply Ee.eval_box; [|now eauto].
              apply eval_to_mkApps_tBox_inv in ev_stuck as ?; subst.
              eauto.
        -- eauto.
        -- rewrite mkApps_snoc.
           eapply PCUICValidity.type_App'; eauto.
           eapply subject_reduction; eauto.
           eapply wcbeval_red; eauto.

  - apply inversion_App in Hty as Hty'; [|eauto].
    destruct Hty' as (? & ? & ? & ? & ? & ?).

    eapply subject_reduction in t as typ_stuck_fix; [|eauto|]; first last.
    { eapply wcbeval_red; eauto. }

    eapply erases_App in He as [(-> & [])|(? & ? & → & ? & ?)].
    + E.tBox.
      split; [|now constructor; eauto using @Ee.eval].
      constructor.
      eapply Is_type_red.
      × eauto.
      × eapply PCUICReduction.red_app.
        -- eapply wcbeval_red; revgoals; eauto.
        -- eapply wcbeval_red; revgoals; eauto.
      × eauto.
    + depelim Hed.
      eapply subject_reduction in t0 as typ_arg; [|eauto|]; first last.
      { eapply wcbeval_red; revgoals; eauto. }

      eapply IHeval1 in H1 as (? & ? & [?]); [|now eauto|now eauto].
      eapply IHeval2 in H2 as (? & ? & [?]); [|now eauto|now eauto].
      eapply erases_mkApps_inv in H1.
      destruct H1 as [(? & ? & ? & → & [] & ? & ? & ->)|(? & ? & → & ? & ?)].
      × apply eval_to_mkApps_tBox_inv in H3 as ?; subst.
        depelim H5.
        rewrite → !app_nil_r in ×.
        cbn in ×.
         E.tBox.
        split; [|now constructor; eauto using @Ee.eval].
        eapply (Is_type_app _ _ _ [av]) in X as [].
        -- constructor.
           apply X.
        -- eauto.
        -- eauto.
        -- cbn.
           eapply PCUICValidity.type_App'; eauto.
      × depelim H1.
        -- (E.tApp (E.mkApps (E.tFix mfix' idx) x7) x5).
           split; [eauto using erases_tApp, erases_mkApps|].
           unfold cunfold_fix in ×.
           destruct (nth_error _ _) eqn:nth; [|congruence].
           eapply All2_nth_error_Some in X as (?&?&[? ? ? ? ?]); [|eauto].
           constructor. eapply Ee.eval_fix_value.
           ++ eauto.
           ++ eauto.
           ++ eauto.
           ++ unfold EGlobalEnv.cunfold_fix. now rewrite e0.
           ++ eapply Forall2_length in H5. noconf e. lia.

        -- E.tBox.
           apply eval_to_mkApps_tBox_inv in H3 as ?; subst.
           split; [|now constructor; eauto using @Ee.eval].
           eapply Is_type_app in X as [].
           ++ constructor.
              rewrite <- mkApps_snoc.
              exact X.
           ++ eauto.
           ++ eauto.
           ++ rewrite mkApps_snoc.
              eapply PCUICValidity.type_App'; eauto.

  - assert (Hty' := Hty).
    eapply inversion_Case in Hty' as [mdecl [idecl [decli [args' [[] ht0]]]]]; auto.
    assert (t0' := scrut_ty).
    pose proof H as Heval.
    eapply subject_reduction_eval in t0' as t1. 2: eauto.
    eapply PCUICValidity.inversion_mkApps in t1 as (? & ? & ?); eauto.
    pose proof (subject_closed t) as clfix.
    assert (htcof : Σ ;;; [] |- tCase ip p (mkApps (tCoFix mfix idx) args) brs : T).
    { eapply subject_reduction; eauto. eapply PCUICReduction.red_case_c.
      eapply wcbeval_red in H; eauto. }
    assert (hredcasecof :
      PCUICReduction.red Σ [] (tCase ip p (mkApps (tCoFix mfix idx) args) brs)
        (tCase ip p (mkApps fn args) brs)).
    { constructor; eapply PCUICReduction.red_cofix_case.
        move: e. rewrite closed_unfold_cofix_cunfold_eq; eauto. }
    assert (htcasefn : Σ ;;; [] |- tCase ip p (mkApps fn args) brs : T).
    { eapply subject_reduction; eauto. }
    assert (hredcasediscrcof :
      PCUICReduction.red Σ [] (tCase ip p discr brs) res).
    { etransitivity. eapply PCUICReduction.red_case_c; tea.
      eapply wcbeval_red in H. tea. eauto.
      etransitivity; tea. eapply wcbeval_red; tea. }
    assert (htunfcof : Σ ;;; [] |- tCase ip p (mkApps fn args) brs : T).
    { eapply subject_reduction; eauto. }
    specialize (IHeval1 _ t0').
    specialize (IHeval2 _ htunfcof).
    eapply inversion_CoFix in t; destruct_sigma t; auto.
    eapply PCUICSpine.typing_spine_strengthen in t0; eauto.
    2:{ now eapply nth_error_all in a; tea. }
    invs He.
    × edestruct IHeval1 as (? & ? & ?); eauto. now depelim Hed.
      depelim Hed.
      destruct (declared_inductive_inj H1 decli). subst mdecl0 idecl0.
      rename H0 into decli'. rename H1 into decli''. rename H2 into er. rename H3 into H0.
      eapply erases_mkApps_inv in H8; eauto.
      destruct H8 as [He|He]; destruct_sigma He.
      -- destruct He as (? & ? & ? & ? & ? & ? & ? & ?). subst.
        destruct H9.
        edestruct IHeval2 as (? & ? & [?]).
        { destruct H2 as [i1]. constructor; eauto.
          rewrite mkApps_app.
          eapply erases_mkApps. instantiate(1:=EAst.tBox).
          constructor.
          eapply isErasable_Proof.
          eapply tCoFix_no_Type in i1; auto.
          pose proof i1 as X0'. destruct X0' as [tyapp [u [Htyapp Hu]]].
          eapply Is_proof_ty; eauto.
          eapply unfold_cofix_type; eauto.
          move: e. rewrite -closed_unfold_cofix_cunfold_eq // /unfold_cofix e0.
          intros e; eapply e. eauto. }
        { destruct (declared_inductive_inj decli'' decli); subst.
          econstructor; eauto. }
        destruct H2.
        eapply tCoFix_no_Type in X0; auto.
        move: (eval_to_mkApps_tBox_inv _ _ H1). intros →. depelim H8.
        rewriteapp_nil_r in ×.
         x0; split; [|constructor]; auto.
        eapply eval_case_eval_inv_discr; tea.
      -- destruct H9.
        destruct He as [f' [L' [-> [hcof hl']]]].
        have clfix' : ELiftSubst.closed f'.
        { now eapply erases_closed in hcof; tea. }
        depelim hcof.
        { eapply All2_nth_error_Some in X0 as X'; tea.
          destruct X' as [t' [nth' [bn [rar eb]]]].
          specialize (IHeval2 (E.tCase (ip, ci_npar ip)
            (E.mkApps (ELiftSubst.subst0 (EGlobalEnv.cofix_subst mfix') (E.dbody t')) L') brs')).
          forward IHeval2.
          econstructor; eauto.
          eapply erases_mkApps.
          move: e0 e. rewrite -closed_unfold_cofix_cunfold_eq //.
          unfold unfold_cofix. intros hnth; rewrite hnth. intros [=].
          subst fn narg.
          eapply All_nth_error in a0 as a'; tea.
          eapply erases_subst0. eauto. 2:eauto. pcuic. all:tea.
          { rewrite app_context_nil_l. eapply subslet_cofix_subst; eauto.
            econstructor; eauto. }
          {eapply All2_from_nth_error.
            erewrite cofix_subst_length, EGlobalEnv.cofix_subst_length, All2_length; eauto.
            intros.
            rewrite cofix_subst_nth in H3. now rewrite cofix_subst_length in H2.
            rewrite ecofix_subst_nth in H8. rewrite cofix_subst_length in H2.
            erewrite <- All2_length; eauto.
            invs H3; invs H8.
            erewrite All2_length; eauto. }
          destruct IHeval2 as [v' [Hv' [ev]]].
          { econstructor; eauto.
            eapply erases_deps_eval in Hed. 2:tea.
            apply erases_deps_mkApps_inv in Hed as (edcofix & edargs).
            depelim edcofix.
            apply erases_deps_mkApps; [|now eauto].
            apply erases_deps_subst.
            - now apply Forall_All, Forall_erases_deps_cofix_subst; eauto.
            - now eapply nth_error_forall in H2; eauto. }
           v'. split ⇒ //. split.
          eapply Ee.eval_cofix_case; tea.
          rewrite /EGlobalEnv.cunfold_cofix nth' //. f_equal.
          f_equal.
          rewrite -(Ee.closed_cofix_substl_subst_eq (idx:=idx)) //. }
        { eapply eval_to_mkApps_tBox_inv in H1 as H'; subst L'; cbn in ×. depelim hl'.
          edestruct IHeval1 as (? & ? & [?]); tea.
          pose proof (Ee.eval_deterministic H1 H3). subst x0.
          eapply erases_deps_eval in Hed; tea.
          specialize (IHeval2 (E.tCase (ip, ci_npar ip) E.tBox brs')).
          forward IHeval2.
          econstructor; eauto. cbn.
          move: e0 e. rewrite -closed_unfold_cofix_cunfold_eq //.
          unfold unfold_cofix. intros hnth; rewrite hnth. intros [=].
          subst fn narg.
          constructor.
          eapply isErasable_unfold_cofix; tea.
          destruct IHeval2 as [v' [Hv' [ev]]].
          { econstructor; eauto. }
           v'. split ⇒ //. split.
          eapply eval_case_eval_inv_discr; tea. }
          
    × depelim Hed.
       E.tBox. split; repeat constructor; auto.
      assert (PCUICReduction.red Σ [] (tCase ip p discr brs) res).
      eapply wcbeval_red in Heval; tea.
      now eapply isErasable_red.

  - assert (Hty' := Hty).
    eapply inversion_Proj in Hty' as (? & ? & ? & ? & [] & ? & ? & ? & e0 & e1); auto.
    pose proof (t0' := t).
    pose proof (subject_closed t) as cldiscr.
    assert(clcof : PCUICAst.closedn 0 (mkApps (tCoFix mfix idx) args)).
    { eapply eval_closed; tea; eauto. }
    move: clcof; rewrite closedn_mkApps ⇒ /andP[] clcofix clargs.
    eapply subject_reduction_eval in t as t0''; tea.
    eapply inversion_mkApps in t0'' as (? & ? & ?).
    eapply type_tCoFix_inv in t0 as t1'; eauto.
    destruct_sigma t1'; auto.
    eapply inversion_CoFix in t0; destruct_sigma t0.
    destruct p0 as [[hnth wfcof] hdef].
    eapply PCUICSpine.typing_spine_strengthen in t1; eauto.
    2:{ now eapply validity. }
    assert(Hty' := Hty).
    eapply subject_reduction in Hty'. 2:auto.
    2:{ etransitivity. eapply PCUICReduction.red_proj_c.
        eapply wcbeval_red; tea.
        constructor. eapply PCUICReduction.red_cofix_proj. eauto.
        rewrite closed_unfold_cofix_cunfold_eq; eauto. }
    specialize (IHeval2 _ Hty').
    specialize (IHeval1 _ t).
    invs He.
    × depelim Hed.
      destruct (declared_projection_inj d H1) as [? [? []]]. subst x0 x1 x2 pdecl.
      rename H1 into decli. rename H2 into decli'.
      rename H3 into erm. rename H4 into erb.
      destruct (IHeval1 _ H6 Hed) as [dv' [? []]].
      eapply erases_mkApps_inv in H1 as []; eauto.
      { destruct H1 as (? & ? & ? & ? & ? & ? & ? & ?). subst.
        destruct H3.
        eapply eval_to_mkApps_tBox_inv in H2 as H'. subst. depelim H7.
        edestruct IHeval2 as (? & ? & [?]).
        { constructor; eauto.
          instantiate(1:=EAst.tBox).
          constructor.
          eapply isErasable_Proof.
          eapply tCoFix_no_Type in X; auto.
          pose proof X as X0'. destruct X0' as [tyapp [u [Htyapp Hu]]].
          eapply Is_proof_ty; eauto.
          move: e. rewrite -closed_unfold_cofix_cunfold_eq // /unfold_cofix e2.
          intros [= <- <-].
          eapply unfold_cofix_type; eauto.
          2:{ unfold unfold_cofix; erewrite e2. reflexivity. }
          now rewrite app_nil_r. }
        { eapply erases_deps_eval in Hed. 2:tea.
          apply erases_deps_mkApps_inv in Hed as (_ & edargs).
          econstructor; eauto. constructor. }
         x1; split; [|constructor]; auto.
        eapply eval_proj_eval_inv_discr; tea. }
      { destruct H1 as [f' [L' [-> [hcof hl']]]].
        have clfix' : ELiftSubst.closed f'.
        { now eapply erases_closed in hcof; tea. }
        depelim hcof.
        { eapply All2_nth_error_Some in X as X'; tea.
          destruct X' as [t' [nth' [bn [rar eb]]]].
          specialize (IHeval2 (E.tProj p
            (E.mkApps (ELiftSubst.subst0 (EGlobalEnv.cofix_subst mfix') (E.dbody t')) L'))).
          forward IHeval2.
          econstructor; eauto.
          eapply erases_mkApps.
          move: hnth e. rewrite -closed_unfold_cofix_cunfold_eq //.
          unfold unfold_cofix. intros hnth'; rewrite hnth'. intros [=].
          subst fn narg. rewrite hnth' in e2. noconf e2.
          eapply All_nth_error in a0 as a'; tea.
          eapply erases_subst0. eauto. 2:eauto. pcuic. all:tea.
          { rewrite app_context_nil_l. eapply subslet_cofix_subst; eauto.
            econstructor; eauto. }
          {eapply All2_from_nth_error.
            erewrite cofix_subst_length, EGlobalEnv.cofix_subst_length, All2_length; eauto.
            intros.
            rewrite cofix_subst_nth in H3. now rewrite cofix_subst_length in H1.
            rewrite ecofix_subst_nth in H4. rewrite cofix_subst_length in H1.
            erewrite <- All2_length; eauto.
            invs H3; invs H4.
            erewrite All2_length; eauto. }
          destruct IHeval2 as [v' [Hv' [ev]]].
          { econstructor; eauto.
            eapply erases_deps_eval in Hed. 2:tea.
            apply erases_deps_mkApps_inv in Hed as (edcofix & edargs).
            depelim edcofix.
            apply erases_deps_mkApps; [|now eauto].
            apply erases_deps_subst.
            - now apply Forall_All, Forall_erases_deps_cofix_subst; eauto.
            - now eapply nth_error_forall in H1; eauto. }
           v'. split ⇒ //. split.
          eapply Ee.eval_cofix_proj; tea.
          rewrite /EGlobalEnv.cunfold_cofix nth' //. f_equal.
          f_equal.
          rewrite -(Ee.closed_cofix_substl_subst_eq (idx:=idx)) //. }
        { eapply eval_to_mkApps_tBox_inv in H2 as H'; subst L'; cbn in ×. depelim hl'.
          edestruct IHeval1 as (? & ? & [?]); tea.
          pose proof (Ee.eval_deterministic H3 H2). subst x0.
          eapply erases_deps_eval in Hed; tea.
          specialize (IHeval2 (E.tProj p E.tBox)).
          forward IHeval2.
          econstructor; eauto. cbn.
          move: hnth e. rewrite -closed_unfold_cofix_cunfold_eq //.
          unfold unfold_cofix. intros hnth; rewrite hnth. intros [=].
          subst fn narg.
          constructor.
          eapply isErasable_unfold_cofix; tea.
          destruct IHeval2 as [v' [Hv' [ev]]].
          { econstructor; eauto. }
           v'. split ⇒ //. split.
          eapply eval_proj_eval_inv_discr; tea. }
      }
    
    × depelim Hed.
       E.tBox. split; repeat constructor; auto.
      assert (PCUICReduction.red Σ [] (tProj p discr) res).
      eapply wcbeval_red in H0; tea.
      etransitivity; tea.
      etransitivity. eapply PCUICReduction.red_proj_c.
      eapply wcbeval_red; tea.
      constructor. eapply PCUICReduction.red_cofix_proj.
      move: e. rewrite closed_unfold_cofix_cunfold_eq //. intros e; exact e.
      now eapply isErasable_red.

    × eauto.

  - pose (Hty' := Hty).
    eapply inversion_App in Hty' as (? & ? & ? & ? & ? & ?); eauto.
    invs He.
    + depelim Hed.
      assert (t' := t). eapply IHeval1 in t as (? & ? & [?]); eauto.
      eapply IHeval2 in t0 as (? & ? & [?]); eauto.
      destruct (EAstUtils.isBox x2) eqn:E.
      × destruct x2; invs E. EAst.tBox. split. 2: now constructor; econstructor; eauto.
        pose proof (Is_type_app Σ [] (mkApps (tConstruct ind c u) args) [a']).
        inversion H1.
        edestruct H7; eauto. cbn. eapply subject_reduction. eauto.
        exact Hty. eapply PCUICReduction.red_app.
        eapply wcbeval_red; eauto.
        eapply inversion_App in Hty as [na [A [B [Hf [Ha _]]]]]; eauto.
        eapply wcbeval_red; eauto. constructor. rewrite mkApps_app //.
      × (E.tApp x2 x3).
        rewrite mkApps_app.
        split; [econstructor; eauto|].
        eapply erases_mkApps_inv in H1; eauto.
        destruct H1 as [].
        { destruct H1 as (? & ? & ? & ? & ? & ? & ? & ?). subst.
          eapply eval_to_mkApps_tBox_inv in H2 as H'. subst. depelim H9.
          now cbn in E. }
        destruct H1 as [f'' [L' [eq []]]].
        subst x2.
        depelim H1.
        2:{ eapply eval_to_mkApps_tBox_inv in H2 as H'. subst. now cbn in E. }
        eapply erases_deps_eval in Hed1; tea.
        eapply erases_deps_mkApps_inv in Hed1 as [].
        depelim H8.
        constructor. eapply Ee.eval_construct; tea. eauto.
        eapply (EGlobalEnv.declared_constructor_lookup H9).
        rewrite -(Forall2_length H7).
        rewrite /EAst.cstr_arity.
        destruct (declared_constructor_inj H8 d) as [? []]. subst mdecl0 idecl0 cdecl0.
        destruct H8, H9, H11 as [Hc _].
        eapply Forall2_nth_error_Some in Hc as [? []]; tea.
        rewrite H14 in H11. noconf H11.
        destruct cdecl' as [cname cargs]; cbn. cbn in ×.
        destruct H15 as [<- _].
        destruct H10 as [_ <-].
        move: l. rewrite /cstr_arity.
        clear -d wfΣ.
        destruct (on_declared_constructor d) as [_ [? []]].
        eapply cstr_args_length in o. lia.
    + E.tBox. split ⇒ //. 2:repeat constructor.
      econstructor.
      eapply inversion_App in Hty as [na [A [B [Hf [Ha _]]]]]; auto.
      eapply Is_type_red. 3:eauto. eauto.
      rewrite mkApps_app.
      eapply PCUICReduction.red_app.
      eapply subject_closed in Hf; auto.
      eapply wcbeval_red; eauto.
      eapply subject_closed in Ha; auto.
      eapply wcbeval_red; eauto.

  - pose (Hty' := Hty).
    eapply inversion_App in Hty' as (? & ? & ? & ? & ? & ?); eauto.
    invs He.
    + depelim Hed.
      assert (t' := t). eapply IHeval1 in t as (? & ? & [?]); eauto.
      eapply IHeval2 in t0 as (? & ? & [?]); eauto.
      destruct (EAstUtils.isBox x2) eqn:E.
      × destruct x2; invs E. EAst.tBox. split. 2: now constructor; econstructor; eauto.
        pose proof (Is_type_app Σ [] f' [a']).
        inversion H1.
        edestruct H7; eauto. cbn. eapply subject_reduction. eauto.
        exact Hty. eapply PCUICReduction.red_app.
        eapply wcbeval_red; eauto.
        eapply inversion_App in Hty as [na [A [B [Hf [Ha _]]]]]; eauto.
        eapply wcbeval_red; eauto.
      × (E.tApp x2 x3).
        split; [econstructor; eauto|].
        constructor; eapply Ee.eval_app_cong; eauto.
        eapply ssrbool.negbT.
        repeat eapply orb_false_intro.
        -- destruct x2; try reflexivity.
          invs H1. invs i.
        -- destruct x2 eqn:Ex; try reflexivity.
          ++ cbn. invs H1. cbn in ×.
            eapply ssrbool.negbTE, is_FixApp_erases.
            econstructor; eauto.
            rewrite orb_false_r !negb_or in i. now move/andP: i ⇒ [].
          ++ cbn in ×.
            invs H1. invs i.
        -- eauto.
        -- rewrite !negb_or in i.
           rtoProp; intuition auto.
           eapply is_ConstructApp_erases in H8; tea.
           now move/negbTE: H8.
    + EAst.tBox. split. 2: now constructor; econstructor.
      econstructor.
      eapply inversion_App in Hty as [na [A [B [Hf [Ha _]]]]]; auto.
      eapply Is_type_red. 3:eauto. eauto.
      eapply PCUICReduction.red_app.
      eapply subject_closed in Hf; auto.
      eapply wcbeval_red; eauto.
      eapply subject_closed in Ha; auto.
      eapply wcbeval_red; eauto.

  - destruct t; try easy.
    + invs He. eexists. split; eauto. now constructor; econstructor.
    + invs He. eexists. split; eauto. now constructor; econstructor.
    + invs He.
      × eexists. split; eauto. now constructor; econstructor.
      × eexists. split. 2: now constructor; econstructor.
        econstructor; eauto.
    + invs He.
      × eexists. split. 2: now constructor; econstructor.
        econstructor; eauto.
    + invs He.
      × eexists. split. 2:{ constructor; econstructor. cbn [EWcbvEval.atom].
        depelim Hed. eapply EGlobalEnv.declared_constructor_lookup in H0. now rewrite H0. }
        econstructor; eauto.
      × eexists. split. 2: now constructor; econstructor.
        eauto.
    + invs He.
      × eexists. split; eauto. now constructor; econstructor.
      × eexists. split. 2: now constructor; econstructor.
        econstructor; eauto.
    + invs He.
      × eexists. split; eauto. now constructor; econstructor.
      × eexists. split. 2: now constructor; econstructor.
        econstructor; eauto.
        Unshelve. all: repeat econstructor.
Qed.


Lemma erases_global_closed_env {Σ : global_env} Σ' : wf Σ erases_global Σ Σ' closed_env Σ'.
Proof.
  destruct Σ as [univs Σ]; cbn in ×.
  intros [onu wf] er; cbn in ×.
  move: wf. red in er; cbn in er.
  induction er; intros wf.
  - constructor.
  - cbn. destruct cb' as [[]].
    cbn in ×. depelim wf.
    rewrite [forallb _ _](IHer wf) andb_true_r.
    red in H. destruct cb as [ty []]; cbn in ×.
    unshelve eapply PCUICClosedTyp.subject_closed in o0. cbn. split; auto.
    eapply erases_closed in H; tea. elim H.
    cbn. apply IHer. now depelim wf.
  - depelim wf.
    cbn. apply IHer, wf.
Qed.

Lemma erases_global_decls_fresh univs {Σ : global_declarations} kn Σ' : fresh_global kn Σ erases_global_decls univs Σ Σ' EGlobalEnv.fresh_global kn Σ'.
Proof.
  induction 2; constructor; eauto; now depelim H.
Qed.

Import EWellformed.

Lemma erases_mutual_inductive_body_wf (efl := all_env_flags) {Σ univs Σ' kn mib mib'} :
  erases_mutual_inductive_body mib mib'
  let udecl := PCUICLookup.universes_decl_of_decl (InductiveDecl mib) in
  on_global_decl cumulSpec0 (PCUICEnvTyping.lift_typing typing) ({| universes := univs; declarations := Σ |}, udecl) kn
       (InductiveDecl mib)
  wf_global_decl Σ' (E.InductiveDecl mib').
Proof.
  intros [] udecl [].
  cbn. unfold wf_minductive ⇒ /=. cbn. clear -H onInductives.
  repeat toAll.
  revert H. subst udecl.
  generalize (E.ind_bodies mib').
  induction onInductives; intros l a; depelim a; constructor; eauto.
  destruct e. unfold wf_inductive, wf_projections.
  destruct H0 as [Hprojs _].
  depelim Hprojs. rewrite H1 ⇒ //.
  rewrite H2.
  pose proof (onProjections p).
  forward X. { congruence. }
  destruct (ind_ctors hd) as [|ctor []] eqn:hctors ⇒ //.
  depelim H. rewrite H1.
  depelim H0. cbn. destruct X.
  destruct H. rewrite -H.
  rewrite H3 in on_projs_all. cbn in on_projs_all.
  eapply Forall2_length in Hprojs. rewrite Hprojs in on_projs_all.
  rewrite on_projs_all.
  pose proof (onConstructors p).
  rewrite hctors in X. red in X.
  depelim X. destruct o. rewrite cstr_args_length.
  apply eqb_refl.
Qed.

Lemma erases_global_wf_glob {Σ : global_env} Σ' : wf Σ erases_global Σ Σ' @wf_glob all_env_flags Σ'.
Proof.
  destruct Σ as [univs Σ]; cbn in ×.
  intros [onu wf] er; cbn in ×.
  move: wf. red in er; cbn in er.
  induction er; intros wf.
  - constructor.
  - cbn. depelim wf.
    constructor; eauto.
    2:eapply erases_global_decls_fresh; tea.
    cbn. red in H.
    do 2 red in o0.
    destruct (cst_body cb).
    destruct (E.cst_body cb') ⇒ //. cbn.
    set (Σ'' := ({| universes := _ |}, _)) in ×.
    assert (PCUICTyping.wf_ext Σ'').
    { split ⇒ //. }
    epose proof (erases_wellformed (Σ:=Σ'') (Γ := []) (a:=t)).
    forward H0. now eexists.
    specialize (H0 H Σ'). eapply H0.
    eapply erases_global_all_deps; tea. split ⇒ //.
    destruct (E.cst_body cb') ⇒ //.
  - depelim wf.
    constructor; eauto.
    now eapply erases_mutual_inductive_body_wf.
    now eapply erases_global_decls_fresh; tea.
Qed.

Import PCUICAst.

Lemma declared_constructor_arity {cf : checker_flags} {Σ c mdecl idecl cdecl} {wf : wf Σ} :
  PCUICAst.declared_constructor Σ c mdecl idecl cdecl
  context_assumptions (cstr_args cdecl) = cstr_arity cdecl.
Proof.
  intros hd.
  destruct (PCUICWeakeningEnvTyp.on_declared_constructor hd) as [[onmind onind] [cu []]].
  now eapply cstr_args_length in o.
Qed.

From MetaCoq.PCUIC Require Import PCUICEtaExpand.
From MetaCoq.Erasure Require Import EDeps EEtaExpandedFix.
Local Hint Constructors expanded : core.

Lemma expanded_erases (cf := config.extraction_checker_flags) {Σ : global_env_ext} Σ' Γ Γ' t v :
  wf Σ
  Σ ;;; Γ |- t v
  PCUICEtaExpand.expanded Σ.1 Γ' t
  erases_deps Σ Σ' v
  EEtaExpandedFix.expanded Σ' Γ' v.
Proof.
  intros wfΣ he exp etaΣ.
  revert Γ v etaΣ he.
  induction exp using PCUICEtaExpand.expanded_ind; cbn.
  all:try solve [intros Γ0 v etaΣ hv; depelim hv; try depelim etaΣ; constructor; solve_all].
  - moveΓ0 etaΣ v /erases_mkApps_inv; intros [(?&?&?&?&?&?&?&?)|(?&?&?&?&?)]; subst.
    × constructor ⇒ //.
      eapply EDeps.erases_deps_mkApps_inv in v as [].
      repeat All_Forall.toAll. eapply All_app in H1 as [].
      solve_all.
    × eapply EDeps.erases_deps_mkApps_inv in v as [].
      depelim H4; simp_eta ⇒ //.
      + eapply expanded_tRel_app; tea. now rewrite -(Forall2_length H5).
        eapply Forall_All in H2. eapply Forall2_All2 in H5. solve_all.
      + constructor ⇒ //. solve_all.
  - intros Γ0 v etaΣ.
    move⇒ /erases_mkApps_inv; intros [(?&?&?&?&?&?&?&?)|(?&?&?&?&?)]; subst.
    × eapply erases_deps_mkApps_inv in etaΣ as [].
      constructor ⇒ //.
      eapply Forall_All in H1. eapply Forall2_All2 in H5.
      eapply All_app in H1 as []. solve_all.
    × eapply erases_deps_mkApps_inv in etaΣ as [].
      specialize (IHexp _ _ H2 H3).
      constructor ⇒ //.
      clear -H H3. destruct H3; cbn in *; congruence.
      solve_all.
  - intros Γ0 v etaΣ hv; depelim hv; try constructor.
    depelim etaΣ.
    eauto.
    depelim etaΣ.
    solve_all. rewrite -b2. len. eapply H7 ⇒ //.
    exact a0.
  - intros Γ0 v etaΣ.
    move⇒ /erases_mkApps_inv; intros [(?&?&?&?&_&?&?&?)|(?&?&?&?&?)]; subst.
    × eapply erases_deps_mkApps_inv in etaΣ as [].
      constructor ⇒ //.
      eapply Forall_All in H2. eapply Forall2_All2 in H8.
      eapply All_app in H2 as []. solve_all.
    × eapply erases_deps_mkApps_inv in etaΣ as [].
      depelim H7; simp_eta ⇒ //.
      + eapply All2_nth_error_Some in H4; tea. destruct H4 as [? [? []]]; tea.
        assert (rev_map (fun d1 : def termS (rarg d1)) mfix = rev_map (fun d1S (EAst.rarg d1)) mfix').
        { rewrite !rev_map_spec. f_equal. clear -X. induction X; cbn; auto. destruct r as [eqb eqrar isl isl' e].
          rewrite eqrar IHX //. }
        depelim H6.
        eapply EEtaExpandedFix.expanded_tFix; tea.
        ++ cbn. rewrite -H6. solve_all. apply b0.
          eapply b1 ⇒ //. eapply b0.
        ++ solve_all.
        ++ intros hx0. subst x0. depelim H8 ⇒ //.
        ++ now rewrite -(Forall2_length H8) -e1.
      + constructor ⇒ //; solve_all.
  - intros Γ0 v etaΣ hv. depelim hv. depelim etaΣ.
    constructor ⇒ //. rewrite -(All2_length X). solve_all. constructor.
  - intros Γ0 v etaΣ.
    move⇒ /erases_mkApps_inv; intros [(?&?&?&?&_&?&?&?)|(?&?&?&?&?)]; subst.
    × eapply erases_deps_mkApps_inv in etaΣ as [].
      constructor ⇒ //.
      eapply Forall_All in H2. eapply Forall2_All2 in H5.
      eapply All_app in H2 as []. solve_all.
    × depelim H4; simp_eta ⇒ //.
      + eapply erases_deps_mkApps_inv in etaΣ as [].
        depelim H4.
        destruct cdecl'.
        eapply EEtaExpandedFix.expanded_tConstruct_app; tea.
        ++ cbn. rewrite -(Forall2_length H5).
          destruct (PCUICGlobalEnv.declared_constructor_inj H H4) as [? []]. subst idecl0 mind cdecl0.
          rewrite (declared_constructor_arity H) in H0.
          destruct H7. rewrite -H10.
          destruct H8 as [? _].
          eapply Forall2_nth_error_left in H8. 2:apply H.
          destruct H8 as [[i' n'] [hnth heq]].
          cbn in hnth.
          rewrite (proj2 H6) in hnth. noconf hnth.
          destruct heq. cbn in ×. congruence.
        ++ solve_all.
        + constructor ⇒ //.
          eapply erases_deps_mkApps_inv in etaΣ as [].
          solve_all.
Qed.