Library MetaCoq.Erasure.ErasureProperties

From Coq Require Import Program ssreflect ssrbool.
From MetaCoq.Template Require Import config utils.
From MetaCoq.Erasure Require Import ELiftSubst EGlobalEnv EWcbvEval Extract Prelim
     ESubstitution EArities EDeps.
From MetaCoq.PCUIC Require Import PCUICTyping PCUICGlobalEnv PCUICAst
  PCUICAstUtils PCUICConversion PCUICSigmaCalculus
  PCUICClosed PCUICClosedTyp
  PCUICWeakeningEnv PCUICWeakeningEnvTyp
  PCUICWeakeningConv PCUICWeakeningTyp PCUICSubstitution PCUICArities
  PCUICWcbvEval PCUICSR PCUICInversion
  PCUICLiftSubst
  PCUICUnivSubstitutionConv PCUICUnivSubstitutionTyp
  PCUICElimination PCUICCanonicity
  PCUICUnivSubst PCUICViews
  PCUICCumulativity PCUICSafeLemmata
  PCUICArities PCUICInductiveInversion
  PCUICContextConversion PCUICContextConversionTyp
  PCUICOnFreeVars PCUICWellScopedCumulativity PCUICValidity
  PCUICContexts PCUICEquality PCUICSpine
  PCUICInductives.
From MetaCoq.PCUIC Require Import PCUICTactics.

Require Import Equations.Prop.DepElim.

Local Set Keyed Unification.

Local Existing Instance config.extraction_checker_flags.


Lemma isLambda_subst_instance t u : isLambda t → isLambda t@[u].
Proof. destruct t ⇒ //. Qed.

Lemma wf_local_rel_conv:
  ∀ Σ : global_env × universes_decl,
    wf Σ.1 →
    ∀ Γ Γ' : context,
      All2_fold (conv_decls cumulAlgo_gen Σ) Γ Γ' →
      ∀ Γ0 : context, wf_local Σ Γ' → wf_local_rel Σ Γ Γ0 → wf_local_rel Σ Γ' Γ0.
Proof.
  intros Σ wfΣ Γ Γ' X1 Γ0 ? w0. induction w0.
  - econstructor.
  - econstructor; eauto. cbn in ×.
    destruct t0. ∃ x. eapply context_conversion with (Γ ,,, Γ0); eauto.
    × eapply wf_local_app; eauto.
    × eapply conv_context_app_same; eauto.
  - econstructor; eauto.
    + cbn in ×.
      destruct t0. ∃ x. eapply context_conversion with (Γ ,,, Γ0); eauto.
      × eapply wf_local_app; eauto.
      × eapply conv_context_app_same; eauto.
    + cbn in ×. eapply context_conversion with (Γ ,,, Γ0); eauto.
      × eapply wf_local_app; eauto.
      × eapply conv_context_app_same; eauto.
Qed.

Lemma conv_context_wf_local_app {A B A'} {Σ : global_env_ext} {wfΣ : wf Σ} :
  wf_local Σ (A ,,, B) → wf_local Σ A' → conv_context cumulAlgo_gen Σ A A' → wf_local Σ (A' ,,, B).
Proof.
  intros wfab wfa' cv.
  eapply wf_local_app ⇒ //.
  eapply wf_local_rel_conv; tea.
  now eapply wf_local_app_inv.
Qed.

Lemma type_closed_subst {Σ t T} u : wf_ext Σ →
  Σ ;;; [] |- t : T →
  subst1 t 0 u = PCUICCSubst.csubst t 0 u.
Proof.
  intros wfΣ tc.
  apply subject_closed in tc; auto.
  rewrite PCUICCSubst.closed_subst; auto.
Qed.

Lemma erases_ext_eq Σ Σ' Γ Γ' t1 t1' t2 t2' :
  Σ ;;; Γ |- t1 ⇝ℇ t2 →
  Σ = Σ'→ Γ = Γ' → t1 = t1' → t2 = t2' →
  Σ' ;;; Γ' |- t1' ⇝ℇ t2'.
Proof.
  intros. now subst.
Qed.

Lemma erases_App (Σ : global_env_ext) Γ f L t :
  erases Σ Γ (tApp f L) t →
  (t = EAst.tBox × squash (isErasable Σ Γ (tApp f L)))
  ∨ ∃ f' L', t = EAst.tApp f' L' ∧
            erases Σ Γ f f' ∧
            erases Σ Γ L L'.
Proof.
  intros. generalize_eqs H.
  revert f L.
  inversion H; intros; try congruence; subst.
  - invs H4. right. repeat eexists; eauto.
  - left. split; eauto. now sq.
Qed.

Lemma erases_mkApps (Σ : global_env_ext) Γ f f' L L' :
  erases Σ Γ f f' →
  Forall2 (erases Σ Γ) L L' →
  erases Σ Γ (mkApps f L) (EAst.mkApps f' L').
Proof.
  intros. revert f f' H; induction H0; cbn; intros; eauto.
  eapply IHForall2. econstructor. eauto. eauto.
Qed.

Lemma erases_mkApps_inv (Σ : global_env_ext) Γ f L t :
  Σ;;; Γ |- mkApps f L ⇝ℇ t →
  (∃ L1 L2 L2', L = L1 ++ L2 ∧
                squash (isErasable Σ Γ (mkApps f L1)) ∧
                erases Σ Γ (mkApps f L1) EAst.tBox ∧
                Forall2 (erases Σ Γ) L2 L2' ∧
                t = EAst.mkApps EAst.tBox L2'
  )
  ∨ ∃ f' L', t = EAst.mkApps f' L' ∧
            erases Σ Γ f f' ∧
            Forall2 (erases Σ Γ) L L'.
Proof.
  intros. revert f H ; induction L; cbn in *; intros.
  - right. ∃ t, []. cbn. repeat split; eauto.
  - eapply IHL in H; eauto.
    destruct H as [ (? & ? & ? & ? & ? & ? & ? & ?) | (? & ? & ? & ? & ?)].
    + subst. left. ∃ (a :: x), x0, x1. destruct H0. repeat split; eauto.
    + subst.
      eapply erases_App in H0 as [ (-> & []) | (? & ? & ? & ? & ?)].
      × left. ∃ [a], L, x0. cbn. repeat split; eauto. now constructor.
      × subst. right. ∃ x1, (x2 :: x0). repeat split; eauto.
Qed.

Lemma is_FixApp_erases Σ Γ t t' :
  Σ;;; Γ |- t ⇝ℇ t' →
  negb (isFixApp t) → negb (EAstUtils.isFixApp t').
Proof.
  induction 1; cbn; try congruence.
  - unfold isFixApp, head in ×. cbn. clear IHerases2.
    cbn. rewrite PCUICAstUtils.fst_decompose_app_rec.
    unfold EAstUtils.isFixApp. now rewrite EAstUtils.head_tApp.
Qed.

Lemma is_ConstructApp_erases Σ Γ t t' :
  Σ;;; Γ |- t ⇝ℇ t' →
  negb (isConstructApp t) → negb (EAstUtils.isConstructApp t').
Proof. induction 1; cbn; try congruence.
- unfold isConstructApp in ×. clear IHerases2.
  cbn. rewrite head_tapp.
  unfold EAstUtils.isConstructApp in ×.
  cbn. now rewrite EAstUtils.head_tApp.
Qed.

Lemma erases_isLambda {Σ Γ t u} :
  Σ ;;; Γ |- t ⇝ℇ u → isLambda t → EAst.isLambda u || EAstUtils.isBox u.
Proof.
  intros hf.
  induction hf ⇒ //.
Qed.

Lemma Is_type_conv_context (Σ : global_env_ext) (Γ : context) t (Γ' : context) :
  wf Σ → wf_local Σ Γ → wf_local Σ Γ' →
  conv_context cumulAlgo_gen Σ Γ Γ' → isErasable Σ Γ t → isErasable Σ Γ' t.
Proof.
  intros.
  destruct X3 as (? & ? & ?). red.
  ∃ x. split. eapply context_conversion. 3:eapply X2. all:eauto.
  destruct s as [? | [u []]].
  - left. eauto.
  - right. ∃ u. split; eauto. eapply context_conversion in X2; eauto.
Qed.

#[global]
Hint Resolve Is_type_conv_context : core.

Lemma erases_context_conversion :
  env_prop
  (fun (Σ : global_env_ext) (Γ : context) (t T : PCUICAst.term) ⇒
      ∀ Γ' : context,
        conv_context cumulAlgo_gen Σ Γ Γ' →
        wf_local Σ Γ' →
        ∀ t', erases Σ Γ t t' → erases Σ Γ' t t')
  (fun Σ Γ ⇒ wf_local Σ Γ)
        .
Proof.
  apply typing_ind_env; intros Σ wfΣ Γ wfΓ; intros **; rename_all_hyps; auto.
  all: match goal with [ H : erases _ _ ?a _ |- ?G ] ⇒ tryif is_var a then idtac else invs H end.
  all: try now (econstructor; eauto).
  - econstructor. eapply h_forall_Γ'0.
    econstructor. eauto. now constructor.
    constructor; auto.
    ∃ s1.
    eapply context_conversion. 3:eauto. all:eauto.
  - econstructor. eauto. eapply h_forall_Γ'1.
    econstructor. eauto. now constructor.
    constructor; auto. ∃ s1.
    eapply context_conversion with Γ; eauto.
    eapply context_conversion with Γ; eauto.
    eassumption.
  - econstructor. eauto. eauto.
    eapply (All2i_All2_All2 X6 X5).
    intros ? ? ? (? & ?) (? & ? & (? & ?) & ? & ?) (? & ?).
    split. 2: assumption.
    rewrite <- (PCUICCasesContexts.inst_case_branch_context_eq a).
    eapply e.
    + rewrite case_branch_type_fst.
      eapply conv_context_app_same; eauto.
    + eapply typing_wf_local.
      eapply context_conversion.
      × exact t1.
      × eapply conv_context_wf_local_app; eauto.
      × eapply conv_context_app_same; eauto.
    + now rewrite case_branch_type_fst (PCUICCasesContexts.inst_case_branch_context_eq a).
  - econstructor.

    eapply All2_impl. eapply All2_All_mix_left. eassumption. eassumption.
    intros. cbn in ×.
    destruct X5 as [[Ht IH] []].
    split; intuition auto.
    eapply IH.
    + subst types.
      eapply conv_context_app_same; auto.
    + eapply conv_context_wf_local_app; eauto.
    + assumption.
  - econstructor.

    eapply All2_impl. eapply All2_All_mix_left. eassumption. eassumption.
    intros. cbn in ×.
    decompose [prod] X2. intuition auto.
    eapply b0.
    + subst types. eapply conv_context_app_same; auto.
    + subst types. eapply conv_context_wf_local_app; eauto.
    + assumption.
Qed.

Lemma isErasable_subst_instance (Σ : global_env_ext) Γ T univs u :
  wf_ext_wk Σ → wf_local Σ Γ →
  wf_local (Σ.1, univs) (subst_instance u Γ) →
  isErasable Σ Γ T →
  consistent_instance_ext (Σ.1,univs) (Σ.2) u →
  isErasable (Σ.1,univs) (subst_instance u Γ) (subst_instance u T).
Proof.
  intros. destruct X2 as (? & ? & [ | (? & ? & ?)]).
  - eapply typing_subst_instance in t; eauto.
    eexists. split.
    + eapply t; tas.
    + left. eapply isArity_subst_instance. eauto.
  - eapply typing_subst_instance in t; eauto.
    eexists. split.
    + eapply t; tas.
    + right.
      eapply typing_subst_instance in t0; eauto.
      eexists. split.
      × eapply t0; tas.
      × now rewrite is_propositional_subst_instance.
Qed.

Lemma fix_context_subst_instance:
  ∀ (mfix : list (BasicAst.def term)) (u : Instance.t),
    map (map_decl (subst_instance u))
        (fix_context mfix) =
    fix_context
      (map
         (map_def (subst_instance u)
                  (subst_instance u)) mfix).
Proof.
  intros mfix. unfold fix_context. intros.
  rewrite map_rev.
  rewrite mapi_map.
  rewrite map_mapi. f_equal. eapply mapi_ext. intros. cbn.
  unfold map_decl. cbn. unfold vass.
  rewrite subst_instance_lift. reflexivity.
Qed.

Lemma erases_subst_instance0
  : env_prop (fun Σ Γ t T ⇒ wf_ext_wk Σ →
                           ∀ t' u univs,
                             wf_local (Σ.1, univs) (subst_instance u Γ) →
      consistent_instance_ext (Σ.1,univs) (Σ.2) u →
    Σ ;;; Γ |- t ⇝ℇ t' →
    (Σ.1,univs) ;;; (subst_instance u Γ) |- subst_instance u t ⇝ℇ t')
    (fun Σ Γ ⇒ wf_local Σ Γ).
Proof.
  apply typing_ind_env; intros; cbn -[subst_instance] in *; auto.
  all: match goal with [ H : erases _ _ ?a _ |- ?G ] ⇒ tryif is_var a then idtac else invs H end.
  all: try now (econstructor; eauto 2 using isErasable_subst_instance).
  - cbn. econstructor.
    eapply H0 in X2; eauto. apply X2.
    cbn. econstructor. eauto. cbn. econstructor.
    eapply typing_subst_instance in X0; eauto. apply snd in X0.
    cbn in X0. destruct X0. refine (t0 _ _ _ _); eauto.
  - cbn. econstructor.
    eapply H0 in X3; eauto.
    eapply H1 in X3; eauto. exact X3.
    cbn. econstructor. eauto. cbn. econstructor.
    eapply typing_subst_instance in X0; eauto. apply snd in X0.
    cbn in X0.
    eapply X0; eauto.
    cbn. eapply typing_subst_instance in X1; eauto. apply snd in X1.
    cbn in X1. eapply X1; eauto.
  - unfold subst_instance.
    cbn [subst_instance_constr]. econstructor; eauto.
    eapply All2_map_left.
    eapply (All2i_All2_All2 X6 X9).
    intros ? ? [] [] (? & ? & (? & ?) & (? & ?)) (? & ?). split.
    2: now cbn in ×.
    cbn -[app_context] in ×. fold (subst_instance u bbody).
    eapply erases_ext_eq.
    2, 4, 5: reflexivity. eapply e; eauto.
    + eapply typing_subst_instance_wf_local; eauto.
      destruct Σ; eassumption.
    + rewrite case_branch_type_fst PCUICCasesContexts.inst_case_branch_context_eq; eauto.
    + rewrite case_branch_type_fst PCUICCasesContexts.inst_case_branch_context_eq; eauto.
      rewrite subst_instance_app. unfold app_context. f_equal.
      now rewrite inst_case_branch_context_subst_instance.
  - assert (Hw : wf_local (Σ.1, univs) (subst_instance u (Γ ,,, types))).
    {
      assert(All (fun d ⇒ isType Σ Γ (dtype d)) mfix).
      eapply (All_impl X0); pcuicfo.
      now destruct X5 as [s [Hs ?]]; ∃ s.
      eapply All_mfix_wf in X5; auto. subst types.

      revert X5. clear - wfΣ wfΓ H2 X2 X3.
      induction 1.
      - eauto.
      - cbn. econstructor; eauto. cbn in ×.
        destruct t0 as (? & ?). eexists.
        cbn. eapply typing_subst_instance in t0; eauto. apply snd in t0. cbn in t0.
        eapply t0; eauto.
      - cbn. econstructor; eauto. cbn in ×.
        destruct t0 as (? & ?). eexists.
        cbn. eapply typing_subst_instance in t0; eauto. apply snd in t0.
        eapply t0; eauto.
        cbn in ×. eapply typing_subst_instance in t1; eauto.
        apply snd in t1. eapply t1. all:eauto.
    }

    cbn. econstructor; eauto.
    eapply All2_map_left.
    eapply All2_impl. eapply All2_All_mix_left. eapply X1.
    exact X4.
    intros; cbn in ×. destruct X5.
    destruct p as [p IH].
    destruct a. split; auto.
    now eapply isLambda_subst_instance.
    eapply IH in e1.
    rewrite subst_instance_app in e1. subst types. 2:eauto.
    eapply erases_ctx_ext. eassumption. unfold app_context.
    f_equal.
    eapply fix_context_subst_instance. all: eauto.

  - assert (Hw : wf_local (Σ.1, univs) (subst_instance u (Γ ,,, types))).
  {
    assert(All (fun d ⇒ isType Σ Γ (dtype d)) mfix).
    eapply (All_impl X0); pcuicfo.
    destruct X5 as [s [Hs ?]]; now ∃ s.
    eapply All_mfix_wf in X5; auto. subst types.

    revert X5. clear - wfΣ wfΓ H2 X2 X3.
    induction 1.
    - eauto.
    - cbn. econstructor; eauto. cbn in ×.
      destruct t0 as (? & ?). eexists.
      cbn. eapply typing_subst_instance in t0; eauto. apply snd in t0. cbn in t0.
      eapply t0; eauto.
    - cbn. econstructor; eauto. cbn in ×.
      destruct t0 as (? & ?). eexists.
      cbn. eapply typing_subst_instance in t0; eauto. apply snd in t0.
      eapply t0; eauto.
      cbn in ×. eapply typing_subst_instance in t1; eauto.
      apply snd in t1. eapply t1. all:eauto.
  }

  cbn. econstructor; eauto.
  eapply All2_map_left.
  eapply All2_impl. eapply All2_All_mix_left. eapply X1.
  exact X4.
  intros; cbn in ×. destruct X5. destruct p0. destruct p0.
  destruct p. repeat split; eauto.
  eapply e2 in e1.
  rewrite subst_instance_app in e1; eauto. subst types. 2:eauto.
  eapply erases_ctx_ext. eassumption. unfold app_context.
  f_equal.
  eapply fix_context_subst_instance. all: eauto.
Qed.

Lemma erases_subst_instance :
  ∀ Σ : global_env_ext, wf_ext_wk Σ →
  ∀ Γ, wf_local Σ Γ →
  ∀ t T, Σ ;;; Γ |- t : T →
    ∀ t' u univs,
  wf_local (Σ.1, univs) (subst_instance u Γ) →
   consistent_instance_ext (Σ.1,univs) (Σ.2) u →
    Σ ;;; Γ |- t ⇝ℇ t' →
    (Σ.1,univs) ;;; (subst_instance u Γ) |- subst_instance u t ⇝ℇ t'.
Proof.
  intros Σ X Γ X0 t T X1 t' u univs H H0 H1.
  unshelve eapply (erases_subst_instance0 Σ _ Γ _ _ _); tea; eauto.
Qed.

Lemma erases_subst_instance'' Σ φ Γ t T u univs t' :
  wf_ext_wk (Σ, univs) →
  (Σ, univs) ;;; Γ |- t : T →
  consistent_instance_ext (Σ, φ) univs u →
  (Σ, univs) ;;; Γ |- t ⇝ℇ t' →
  (Σ, φ) ;;; subst_instance u Γ
            |- subst_instance u t ⇝ℇ t'.
Proof.
  intros X X0. intros.
  eapply (erases_subst_instance (Σ, univs)); tas.
  eapply typing_wf_local; eassumption. eauto.
  eapply typing_wf_local.
  eapply typing_subst_instance''; eauto.
Qed.

Lemma erases_subst_instance_decl Σ Γ t T c decl u t' :
  wf Σ.1 →
  lookup_env Σ.1 c = Some decl →
  (Σ.1, universes_decl_of_decl decl) ;;; Γ |- t : T →
  consistent_instance_ext Σ (universes_decl_of_decl decl) u →
  (Σ.1, universes_decl_of_decl decl) ;;; Γ |- t ⇝ℇ t' →
   Σ ;;; subst_instance u Γ
            |- subst_instance u t ⇝ℇ t'.
Proof.
  destruct Σ as [Σ φ]. intros X X0 X1 X2.
  eapply erases_subst_instance''; tea. split; tas.
  eapply weaken_lookup_on_global_env'; tea.
Qed.

Lemma erases_closed Σ Γ a e : PCUICAst.closedn #|Γ| a → Σ ;;; Γ |- a ⇝ℇ e → ELiftSubst.closedn #|Γ| e.
Proof.
  remember #|Γ| as Γl eqn:Heq.
  intros cla era.
  revert Γ e era Heq.
  pattern Γl, a.
  match goal with
  |- ?P Γl a ⇒ simpl; eapply (term_closedn_list_ind P); auto; clear
  end; simpl; intros; subst k;
    match goal with [H:erases _ _ _ _ |- _] ⇒ depelim H end; trivial;
    simpl; try solve [solve_all].
  - now apply Nat.ltb_lt.
  - apply andb_and. split; eauto.
    eapply All_forallb. unfold tCaseBrsProp_k in X0.
    eapply All2_All_mix_left in X1; eauto.
    close_Forall. intros [] []. cbn in ×. intros.
    solve_all. subst. rewrite map_length. eapply b0. eauto.
    rewrite app_context_length. cbn.
    now rewrite inst_case_branch_context_length.
  - epose proof (All2_length X0).
    solve_all. destruct b. destruct y ; simpl in *; subst.
    unfold EAst.test_def; simpl; eauto.
    rewrite <-H. rewrite fix_context_length in b0.
    eapply b0. eauto. now rewrite app_length fix_context_length.
  - epose proof (All2_length X0).
    solve_all. destruct y ; simpl in *; subst.
    unfold EAst.test_def; simpl; eauto.
    rewrite <-H. rewrite fix_context_length in b0.
    eapply b0. eauto. now rewrite app_length fix_context_length.
Qed.

Section wellscoped.
  Import PCUICAst PCUICGlobalEnv.

  Definition lookup_constant Σ kn :=
    match PCUICEnvironment.lookup_env Σ kn with
    | Some (ConstantDecl d) ⇒ Some d
    | _ ⇒ None
    end.
  Import MCMonadNotation.

  Section Def.
  Context (Σ : global_env).
  Import ssrbool.

  Fixpoint wellformed (t : term) : bool :=
  match t with
  | tRel i ⇒ true
  | tEvar ev args ⇒ List.forallb (wellformed) args
  | tLambda _ N M ⇒ wellformed N && wellformed M
  | tApp u v ⇒ wellformed u && wellformed v
  | tLetIn na b ty b' ⇒ wellformed b && wellformed ty && wellformed b'
  | tCase ind p c brs ⇒
    let brs' := forallb (wellformed ∘ bbody) brs in
    isSome (lookup_inductive Σ ind.(ci_ind)) && wellformed c && brs'
  | tProj p c ⇒ isSome (lookup_projection Σ p) && wellformed c
  | tFix mfix idx ⇒
    (idx <? #|mfix|) &&
    List.forallb (test_def (wellformed) (fun b ⇒ (isLambda b) && wellformed b)) mfix
  | tCoFix mfix idx ⇒
    (idx <? #|mfix|) &&
    List.forallb (test_def wellformed wellformed) mfix
  | tConst kn _ ⇒ isSome (lookup_constant Σ kn)
  | tConstruct ind c _ ⇒ isSome (lookup_constructor Σ ind c)
  | tVar _ ⇒ true
  | tInd ind _ ⇒ isSome (lookup_inductive Σ ind)
  | tSort _ ⇒ true
  | tProd na ty1 ty2 ⇒ wellformed ty1 && wellformed ty2
  end.
  End Def.

  Arguments lookup_projection : simpl never.
  Lemma typing_wellformed :
    env_prop (fun Σ Γ a A ⇒ wellformed Σ a)
        (fun Σ Γ ⇒ True).
  Proof.
    eapply typing_ind_env; cbn; intros ⇒ //.
    all:try rtoProp; intuition auto.
    - red in H0. rewrite /lookup_constant H0 //.
    - now rewrite (declared_inductive_lookup isdecl).
    - rewrite (declared_constructor_lookup isdecl) //.
    - now rewrite (declared_inductive_lookup isdecl).
    - red in H8. eapply Forall2_All2 in H8.
      eapply All2i_All2_mix_left in X4; tea. clear H8.
      solve_all.
    - now rewrite (declared_projection_lookup isdecl).
    - now eapply nth_error_Some_length, Nat.ltb_lt in H0.
    - move/andb_and: H2 ⇒ [] hb _.
      solve_all. destruct a as [s []], a0.
      unfold test_def. len in b0.
      rewrite b0. now rewrite i i0.
    - now eapply nth_error_Some_length, Nat.ltb_lt in H0.
    - solve_all. destruct a as [s []], b.
      unfold test_def. len in i0. now rewrite i i0.
  Qed.

  Lemma welltyped_wellformed {Σ : global_env_ext} {wfΣ : wf Σ} {Γ a} : welltyped Σ Γ a → wellformed Σ a.
  Proof.
    intros []. eapply typing_wellformed; tea.
  Qed.

End wellscoped.

Import EWellformed.

Section trans_lookups.
  Context {Σ : global_env_ext} {Σ'} (g : globals_erased_with_deps Σ Σ').

  Lemma trans_lookup_constant kn : isSome (lookup_constant Σ kn) → isSome (EGlobalEnv.lookup_constant Σ' kn).
  Proof using g.
    unfold lookup_constant.
    destruct (lookup_env Σ kn) as [[]|] eqn:hl ⇒ //.
    eapply g in hl as [? []].
    now rewrite (EGlobalEnv.declared_constant_lookup H).
  Qed.

  Lemma trans_lookup_inductive kn : isSome (lookup_inductive Σ kn) → isSome (EGlobalEnv.lookup_inductive Σ' kn).
  Proof using g.
    destruct g.
    destruct (lookup_inductive Σ kn) as [[]|] eqn:hl ⇒ /= // _.
    eapply lookup_inductive_declared in hl.
    specialize (H0 kn m o hl) as [? [? [d _]]].
    now rewrite (EGlobalEnv.declared_inductive_lookup d).
  Qed.

  Lemma trans_lookup_constructor kn c : isSome (lookup_constructor Σ kn c) → isSome (EGlobalEnv.lookup_constructor Σ' kn c).
  Proof using g.
    destruct g.
    destruct (lookup_constructor Σ kn c) as [[[]]|] eqn:hl ⇒ /= // _.
    eapply (lookup_constructor_declared (id:=(kn,c))) in hl.
    specialize (H0 _ _ _ hl) as [mdecl' [idecl' [decli hl']]].
    destruct hl', hl. cbn in × |-.
    destruct H2. eapply Forall2_nth_error_left in H0 as [? [? [erc erp]]]; tea.
    eapply Forall2_nth_error_left in erc as [? [? ?]]; tea.
    destruct decli as [declm decli]. rewrite H0 in decli. noconf decli.
    erewrite (EGlobalEnv.declared_constructor_lookup (id:=(kn,c))) ⇒ //.
    split; tea. split; tea.
  Qed.

  Lemma lookup_projection_lookup_constructor {p mdecl idecl cdecl pdecl} :
    lookup_projection Σ p = Some (mdecl, idecl, cdecl, pdecl) →
    lookup_constructor Σ p.(proj_ind) 0 = Some (mdecl, idecl, cdecl).
  Proof using Type.
    rewrite /lookup_projection; destruct lookup_constructor as [[[? ?] ?]|]=> //=.
    now destruct nth_error ⇒ //.
  Qed.

  Lemma trans_lookup_projection p :
    isSome (lookup_projection Σ p) →
    isSome (EGlobalEnv.lookup_projection Σ' p).
  Proof using g.
    destruct g.
    destruct (lookup_projection Σ p) as [[[[]]]|] eqn:hl ⇒ /= // _.
    pose proof (lookup_projection_lookup_constructor hl) as lc.
    unfold lookup_projection in hl. rewrite lc in hl.
    eapply (lookup_constructor_declared (id:=(_,_))) in lc.
    specialize (H0 _ _ _ lc) as [mdecl' [idecl' [decli hl']]].
    destruct hl', lc.
    destruct H2.
    destruct (nth_error (ind_projs o)) eqn:hnth ⇒ //. noconf hl.
    eapply Forall2_nth_error_left in H0 as [? [? [erc [erp ?]]]]; tea.
    destruct decli. rewrite H7 in H0; noconf H0.
    eapply Forall2_nth_error_left in erc as [? [? ?]]; tea.
    eapply Forall2_nth_error_left in erp as [? [? ?]]; tea.
    rewrite /EGlobalEnv.lookup_projection /EGlobalEnv.lookup_constructor /EGlobalEnv.lookup_inductive.
    rewrite (EGlobalEnv.declared_minductive_lookup H6); cbn -[nth_error]; rewrite H7 H0 H9 //.
  Qed.

End trans_lookups.

Lemma erases_wellformed {Σ : global_env_ext} {wfΣ : wf Σ} {Γ a e} : welltyped Σ Γ a → Σ ;;; Γ |- a ⇝ℇ e →
  ∀ Σ', globals_erased_with_deps Σ Σ' → @EWellformed.wellformed EWellformed.all_env_flags Σ' #|Γ| e.
Proof.
  intros wf.
  generalize (welltyped_wellformed wf).
  destruct wf. eapply subject_closed in X. move: X.
  remember #|Γ| as Γl eqn:Heq.
  intros cla wfa era.
  revert Γ e wfa era Heq.
  pattern Γl, a.
  match goal with
  |- ?P Γl a ⇒ simpl; eapply (term_closedn_list_ind P); auto; clear
  end; simpl; intros; subst k;
    match goal with [H:erases _ _ _ _ |- _] ⇒ depelim H end; trivial;
    simpl; try solve [solve_all].
  - now apply Nat.ltb_lt.
  - eapply trans_lookup_constant in wfa; tea.
  - eapply trans_lookup_constructor in wfa; tea. now rewrite wfa.
  - move/andP: wfa ⇒ [] /andP[] lookup wfc wfbrs.
    apply/andP. split. apply/andP. split; eauto.
    eapply trans_lookup_inductive; tea.
    eapply All_forallb. unfold tCaseBrsProp_k in X0.
    eapply All2_All_mix_left in X1; eauto.
    eapply forallb_All in wfbrs.
    eapply All2_All_mix_left in X1; eauto.
    close_Forall. intros [] []; move⇒ [] wf. cbn in ×. intros.
    solve_all. subst. rewrite map_length. eapply b; eauto.
    rewrite app_context_length. cbn.
    now rewrite inst_case_branch_context_length.
  - move/andP: wfa ⇒ [] hl hc.
    apply/andP; split.
    now eapply trans_lookup_projection in hl.
    eauto.
  - epose proof (All2_length X0).
    unfold EWellformed.wf_fix_gen.
    rewrite -H0. move/andP: wfa ⇒ [] →.
    move/forallb_All. cbn. intros wfa.
    solve_all. destruct b.
    destruct y ; simpl in *; subst.
    unfold EAst.test_def; simpl; eauto.
    rewrite fix_context_length in b1.
    move/andP: b0 ⇒ //; eauto. move⇒ [] wft /andP[] isl wf; eauto.
    eapply b1; tea. now rewrite app_length fix_context_length.
  - epose proof (All2_length X0).
    unfold EWellformed.wf_fix_gen.
    rewrite -H0. move/andP: wfa ⇒ [] →.
    move/forallb_All. cbn. intros wfa.
    solve_all. destruct y ; simpl in *; subst.
    unfold EAst.test_def; simpl; eauto.
    rewrite fix_context_length in b.
    eapply b. now move: b0 ⇒ /andP[]. eauto. now rewrite app_length fix_context_length. tea.
Qed.

Lemma eval_empty_brs {wfl : Ee.WcbvFlags} Σ ci p e : Σ ⊢ E.tCase ci p [] ▷ e → False.
Proof.
  intros He.
  depind He.
  - clear -e1. now rewrite nth_error_nil in e1.
  - clear -e1. now rewrite nth_error_nil in e1.
  - discriminate.
  - eapply IHHe2.
  - cbn in i. discriminate.
Qed.

Lemma eval_case_tBox_inv {wfl : Ee.WcbvFlags} {Σ ci e brs} :
  Σ ⊢ E.tCase ci EAst.tBox brs ▷ e →
  ∑ n br, brs = [(n, br)] × inductive_isprop_and_pars Σ ci.1 = Some (true, ci.2) ×
  Σ ⊢ ECSubst.substl (repeat EAst.tBox #|n|) br ▷ e.
Proof.
  intros He.
  depind He.
  - depelim He1. clear -H. symmetry in H. elimtype False.
    destruct args using rev_case. discriminate.
    rewrite EAstUtils.mkApps_app in H. discriminate.
  - depelim He1.
  - ∃ n, f. intuition auto.
  - depelim He1. clear -H. symmetry in H. elimtype False.
    destruct args using rev_case. discriminate.
    rewrite EAstUtils.mkApps_app in H. discriminate.
  - cbn in i. discriminate.
Qed.

Lemma eval_case_eval_discr {wfl : Ee.WcbvFlags} {Σ ci c c' e brs} :
  Σ ⊢ E.tCase ci c brs ▷ e →
  Σ ⊢ c ▷ c' →
  Σ ⊢ E.tCase ci c' brs ▷ e.
Proof.
  intros He Hc.
  depind He.
  - pose proof (Ee.eval_deterministic He1 Hc). subst c'.
    econstructor; eauto. now eapply Ee.value_final, Ee.eval_to_value.
  - pose proof (Ee.eval_deterministic He1 Hc). subst c'.
    eapply Ee.eval_iota_block; eauto. now eapply Ee.value_final, Ee.eval_to_value.
  - pose proof (Ee.eval_deterministic He1 Hc). subst c'.
    eapply Ee.eval_iota_sing; tea. now constructor.
  - pose proof (Ee.eval_deterministic He1 Hc). subst c'.
    eapply Ee.eval_cofix_case; tea.
    now eapply Ee.value_final, Ee.eval_to_value.
  - cbn in i. discriminate.
Qed.

Lemma eval_case_eval_inv_discr {wfl : Ee.WcbvFlags} {Σ ci c c' e brs} :
  Σ ⊢ E.tCase ci c brs ▷ e →
  Σ ⊢ c' ▷ c →
  Σ ⊢ E.tCase ci c' brs ▷ e.
Proof.
  intros He Hc.
  depind He.
  - pose proof (eval_trans' Hc He1); subst discr.
    econstructor; eauto.
  - pose proof (eval_trans' Hc He1); subst discr.
    now econstructor; eauto.
  - pose proof (eval_trans' Hc He1); subst discr.
    eapply Ee.eval_iota_sing; tea.
  - pose proof (eval_trans' Hc He1); subst discr.
    eapply Ee.eval_cofix_case; tea.
  - cbn in i. discriminate.
Qed.

Lemma eval_proj_eval_inv_discr {wfl : Ee.WcbvFlags} {Σ p c c' e} :
  Σ ⊢ E.tProj p c ▷ e →
  Σ ⊢ c' ▷ c →
  Σ ⊢ E.tProj p c' ▷ e.
Proof.
  intros He Hc.
  depind He.
  - pose proof (eval_trans' Hc He1); subst discr.
    econstructor; eauto.
  - pose proof (eval_trans' Hc He1); subst discr.
    now econstructor; tea.
  - pose proof (eval_trans' Hc He1); subst discr.
    now econstructor; tea.
  - pose proof (eval_trans' Hc He); subst discr.
    now econstructor; tea.
  - cbn in i. discriminate.
Qed.