Mctt.Core.Soundness.LogicalRelation.CoreLemmas

From Coq Require Import Equivalence Morphisms Morphisms_Prop Morphisms_Relations Relation_Definitions RelationClasses.

From Mctt Require Import LibTactics.
From Mctt.Core Require Import Base.
From Mctt.Core.Soundness.LogicalRelation Require Import CoreTactics Definitions.
From Mctt.Core.Soundness.Weakening Require Export Lemmas.
Import Domain_Notations.

Lemma mk_glu_bot_nat : forall Γ M m,
    {{ Dom m ≈ m ∈ per_bot }} ->
    (forall Δ σ M', {{ Δ ⊢w σ : Γ }} -> {{ Rne m in length Δ ↘ M' }} -> {{ Δ ⊢ M[σ] ≈ M' : ℕ }}) ->
    {{ Γ ⊢ M : ℕ ® m ∈ glu_bot }}.
Proof.
  intros.
  econstructor; mauto 3.
  intros.
  assert {{ Δ ⊢ ℕ[σ] ≈ ℕ : Type@0 }} as ->; mauto 3.
Qed.

#[export]
Hint Resolve mk_glu_bot_nat : mctt.

Lemma mk_glu_bot_typ : forall Γ i M m,
    {{ Dom m ≈ m ∈ per_bot }} ->
    (forall Δ σ M', {{ Δ ⊢w σ : Γ }} -> {{ Rne m in length Δ ↘ M' }} -> {{ Δ ⊢ M[σ] ≈ M' : Type@i }}) ->
    {{ Γ ⊢ M : Type@i ® m ∈ glu_bot }}.
Proof.
  intros.
  econstructor; mauto 3.
  intros.
  assert {{ Δ ⊢ Type@i[σ] ≈ Type@i : Type@(S i) }} as ->; mauto 3.
Qed.

#[export]
Hint Resolve mk_glu_bot_typ : mctt.

Lemma glu_bot_nat_inversion : forall Γ M m,
    {{ Γ ⊢ M : ℕ ® m ∈ glu_bot }} ->
    {{ Dom m ≈ m ∈ per_bot }} /\
      (forall Δ σ M', {{ Δ ⊢w σ : Γ }} -> {{ Rne m in length Δ ↘ M' }} -> {{ Δ ⊢ M[σ] ≈ M' : ℕ }}).
Proof.
  destruct 1.
  econstructor; mauto 3.
  intros.
  assert {{ Δ ⊢ ℕ[σ] ≈ ℕ : Type@0 }} as <-; mauto 3.
Qed.

Lemma glu_bot_typ_inversion : forall Γ i M m,
    {{ Γ ⊢ M : Type@i ® m ∈ glu_bot }} ->
    {{ Dom m ≈ m ∈ per_bot }} /\
      (forall Δ σ M', {{ Δ ⊢w σ : Γ }} -> {{ Rne m in length Δ ↘ M' }} -> {{ Δ ⊢ M[σ] ≈ M' : Type@i }}).
Proof.
  destruct 1.
  econstructor; mauto 3.
  intros.
  assert {{ Δ ⊢ Type@i[σ] ≈ Type@i : Type@(S i) }} as <-; mauto 3.
Qed.

Ltac invert_glu_bot H :=
  (unshelve eapply (glu_bot_typ_inversion _ _ _ _) in H; shelve_unifiable; destruct H as [])
  + (unshelve eapply (glu_bot_nat_inversion _ _ _) in H; shelve_unifiable; destruct H as [])
  + dependent inversion H.

Ltac invert_glu_bots := match_by_head glu_bot invert_glu_bot.

Lemma glu_bot_escape : forall Γ A M m,
    {{ Γ ⊢ M : A ® m ∈ glu_bot }} ->
    {{ ⊢ Γ }} ->
    {{ Γ ⊢ M : A }}.
Proof.
  destruct 1; intros.
  assert {{ Γ ⊢w Id : Γ }} by mauto.
  match_by_head (per_bot m m) ltac:(fun H => specialize (H (length Γ)) as [M' []]).
  assert {{ Γ ⊢ M[Id] ≈ M' : A[Id] }} by mauto 3.
  gen_presups.
  mauto 3.
Qed.

#[export]
Hint Resolve glu_bot_escape : mctt.

Lemma glu_bot_resp_ctx_eq : forall Γ Δ,
    {{ ⊢ Γ ≈ Δ }} ->
    forall A M m,
      {{ Γ ⊢ M : A ® m ∈ glu_bot }} ->
      {{ Δ ⊢ M : A ® m ∈ glu_bot }}.
Proof.
  destruct 2; intros.
  econstructor; intros; try eassumption.
  intuition mauto 4.
Qed.

#[local]
Hint Resolve glu_bot_resp_ctx_eq : mctt.

Add Parametric Morphism : glu_bot
    with signature wf_ctx_eq ==> eq ==> eq ==> eq ==> iff as glu_bot_morphism_iff1.
Proof.
  split; mauto 3.
Qed.

Lemma glu_bot_resp_typ_exp_eq : forall Γ A A' i,
    {{ Γ ⊢ A ≈ A' : Type@i }} ->
    forall M m,
      {{ Γ ⊢ M : A ® m ∈ glu_bot }} ->
      {{ Γ ⊢ M : A' ® m ∈ glu_bot }}.
Proof.
  destruct 2; intros.
  econstructor; intros; try eassumption.
  assert {{ Δ ⊢ M[σ] ≈ M' : A[σ] }}; mauto 4.
Qed.

#[local]
Hint Resolve glu_bot_resp_typ_exp_eq : mctt.

Add Parametric Morphism Γ i : (glu_bot Γ)
    with signature wf_exp_eq Γ {{{ Type@i }}} ==> eq ==> eq ==> iff as glu_bot_morphism_iff2.
Proof.
  split; mauto 3.
Qed.

Lemma glu_bot_resp_exp_eq : forall Γ A M M',
    {{ Γ ⊢ M ≈ M' : A }} ->
    forall m,
      {{ Γ ⊢ M : A ® m ∈ glu_bot }} ->
      {{ Γ ⊢ M' : A ® m ∈ glu_bot }}.
Proof.
  destruct 2; intros.
  econstructor; intros; try eassumption.
  transitivity {{{ M[σ] }}}; [mauto | mauto 2].
Qed.

#[local]
Hint Resolve glu_bot_resp_exp_eq : mctt.

Add Parametric Morphism Γ A : (glu_bot Γ A)
    with signature wf_exp_eq Γ A ==> eq ==> iff as glu_bot_morphism_iff3.
Proof.
  split; mauto 3.
Qed.

Lemma glu_bot_resp_per_bot : forall m n,
    {{ Dom m ≈ n ∈ per_bot }} ->
    forall Γ A M,
      {{ Γ ⊢ M : A ® m ∈ glu_bot }} ->
      {{ Γ ⊢ M : A ® n ∈ glu_bot }}.
Proof.
  intros * H.
  destruct 1; intros.
  econstructor; intros; mauto 3.
  specialize (H (length Δ)) as [? []].
  functional_read_rewrite_clear.
  mauto 3.
Qed.

#[local]
Hint Resolve glu_bot_resp_per_bot : mctt.

Add Parametric Morphism Γ A M : (glu_bot Γ A M)
    with signature per_bot ==> iff as glu_bot_morphism_iff4.
Proof.
  split; mauto 3.
Qed.

Lemma glu_bot_typ_readback : forall Γ i M m,
    {{ Γ ⊢ M : Type@i ® m ∈ glu_bot }} ->
    forall Δ σ M',
      {{ Δ ⊢w σ : Γ }} ->
      {{ Rne m in length Δ ↘ M' }} ->
      {{ Δ ⊢ M[σ] ≈ M' : Type@i }}.
Proof.
  intros * H.
  invert_glu_bot H.
  intros; mauto 3.
Qed.

Lemma glu_bot_nat_readback : forall Γ M m,
    {{ Γ ⊢ M : ℕ ® m ∈ glu_bot }} ->
    forall Δ σ M',
      {{ Δ ⊢w σ : Γ }} ->
      {{ Rne m in length Δ ↘ M' }} ->
      {{ Δ ⊢ M[σ] ≈ M' : ℕ }}.
Proof.
  intros * H.
  invert_glu_bot H.
  intros; mauto 3.
Qed.

Lemma glu_bot_resp_wk' : forall Γ A M m,
    {{ Γ ⊢ M : A ® m ∈ glu_bot }} ->
    forall Δ σ,
      {{ Γ ⊢ M : A }} ->
      {{ Δ ⊢w σ : Γ }} ->
      {{ Δ ⊢ M[σ] : A[σ] ® m ∈ glu_bot }}.
Proof.
  destruct 1; intros.
  econstructor; mauto 3.
  intros Δ' τ M' **.
  gen_presups.
  assert {{ Δ' ⊢w σ∘τ : Γ }} by mauto.
  assert {{ Δ' ⊢ M[σ∘τ] ≈ M' : A[σ∘τ] }} by mauto 4.
  autorewrite with mctt.
  transitivity {{{ M[σ∘τ] }}}; [symmetry |]; mauto 4.
Qed.

Lemma glu_bot_resp_wk : forall Γ A M m,
    {{ Γ ⊢ M : A ® m ∈ glu_bot }} ->
    forall Δ σ,
      {{ Δ ⊢w σ : Γ }} ->
      {{ Δ ⊢ M[σ] : A[σ] ® m ∈ glu_bot }}.
Proof.
  intros.
  assert {{ ⊢ Γ }} by mauto 3.
  mauto 3 using glu_bot_resp_wk'.
Qed.

#[export]
Hint Resolve glu_bot_resp_wk : mctt.

Lemma glu_nat_per_nat : forall Γ M m,
    glu_nat Γ M m ->
    {{ Dom m ≈ m ∈ per_nat }}.
Proof.
  induction 1; invert_glu_bots; mauto.
Qed.

#[local]
Hint Resolve glu_nat_per_nat : mctt.

Lemma glu_nat_escape : forall Γ M m,
    glu_nat Γ M m ->
    {{ ⊢ Γ }} ->
    {{ Γ ⊢ M : ℕ }}.
Proof.
  induction 1; intros;
    try match goal with
      | H : _ |- _ => solve [gen_presup H; mauto]
      end.
  mauto.
Qed.

#[export]
Hint Resolve glu_nat_escape : mctt.

Lemma glu_nat_resp_ctx_eq : forall Γ M m Δ,
    glu_nat Γ M m ->
    {{ ⊢ Γ ≈ Δ }} ->
    glu_nat Δ M m.
Proof.
  induction 1; intros; mauto.
Qed.

#[local]
Hint Resolve glu_nat_resp_ctx_eq : mctt.

Add Parametric Morphism : glu_nat
    with signature wf_ctx_eq ==> eq ==> eq ==> iff as glu_nat_morphism_iff1.
Proof.
  split; mauto 3.
Qed.

Lemma glu_nat_resp_exp_eq : forall Γ M m,
    glu_nat Γ M m ->
    forall M',
    {{ Γ ⊢ M ≈ M' : ℕ }} ->
    glu_nat Γ M' m.
Proof.
  induction 1; intros; mauto 4.
Qed.

#[local]
Hint Resolve glu_nat_resp_exp_eq : mctt.

Add Parametric Morphism Γ : (glu_nat Γ)
    with signature wf_exp_eq Γ {{{ ℕ }}} ==> eq ==> iff as glu_nat_morphism_iff2.
Proof.
  split; mauto 3.
Qed.

Lemma glu_nat_resp_per_nat : forall m n,
    {{ Dom m ≈ n ∈ per_nat }} ->
    forall Γ M,
      glu_nat Γ M m ->
      glu_nat Γ M n.
Proof.
  induction 1; intros; progressive_inversion; mauto 3.
Qed.

#[local]
Hint Resolve glu_nat_resp_per_nat : mctt.

Add Parametric Morphism Γ M : (glu_nat Γ M)
    with signature per_nat ==> iff as glu_nat_morphism_iff3.
Proof.
  split; mauto 3.
Qed.

Lemma glu_nat_readback : forall Γ M m,
    glu_nat Γ M m ->
    forall Δ σ M',
      {{ Δ ⊢w σ : Γ }} ->
      {{ Rnf ⇓ ℕ m in length Δ ↘ M' }} ->
      {{ Δ ⊢ M[σ] ≈ M' : ℕ }}.
Proof.
  induction 1; intros; progressive_inversion; gen_presups.
  - transitivity {{{ zero[σ] }}}; mauto 4.
  - assert {{ Δ ⊢ M'[σ] ≈ M0 : ℕ }} by mauto 4.
    transitivity {{{ (succ M')[σ] }}}; mauto 3.
    transitivity {{{ succ M'[σ] }}}; mauto 4.
  - mauto 3 using glu_bot_nat_readback.
Qed.

Lemma glu_nat_resp_wk : forall Γ M a,
    glu_nat Γ M a ->
    forall Δ σ,
      {{ Δ ⊢w σ : Γ }} ->
      glu_nat Δ {{{ M[σ] }}} a.
Proof.
  induction 1; intros; gen_presups; econstructor; mauto 3.
  - transitivity {{{ zero[σ] }}}; mauto 3.
  - transitivity {{{ (succ M')[σ] }}}; [mauto 3 | mauto 4].
  - assert {{ Δ ⊢ ℕ[σ] ≈ ℕ : Type@0 }} as <- by mauto 3.
    mauto 3.
Qed.

#[export]
Hint Resolve glu_nat_resp_wk : mctt.

#[global]
Ltac simpl_glu_rel :=
  apply_equiv_left;
  repeat invert_glu_rel1;
  apply_equiv_left;
  destruct_all;
  gen_presups.

Lemma glu_univ_elem_univ_lvl : forall i P El a,
    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
    forall Γ A,
      {{ Γ ⊢ A ® P }} ->
      {{ Γ ⊢ A : Type@i }}.
Proof.
  simpl.
  induction 1 using glu_univ_elem_ind; intros;
    simpl_glu_rel; trivial.
Qed.

Lemma glu_univ_elem_typ_resp_exp_eq : forall i P El a,
    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
    forall Γ A A',
      {{ Γ ⊢ A ® P }} ->
      {{ Γ ⊢ A ≈ A' : Type@i }} ->
      {{ Γ ⊢ A' ® P }}.
Proof.
  simpl.
  induction 1 using glu_univ_elem_ind; intros;
    simpl_glu_rel; mauto 4.
Qed.

Add Parametric Morphism i P El a (H : glu_univ_elem i P El a) Γ : (P Γ)
    with signature wf_exp_eq Γ {{{ Type@i }}} ==> iff as glu_univ_elem_typ_morphism_iff1.
Proof.
  split; intros; eapply glu_univ_elem_typ_resp_exp_eq; mauto 2.
Qed.

#[global]
Ltac destruct_glu_eq :=
  match_by_head1 glu_eq ltac:(fun H => dependent destruction H).

Lemma glu_univ_elem_trm_resp_typ_exp_eq : forall i P El a,
    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
    forall Γ M A m A',
      {{ Γ ⊢ M : A ® m ∈ El }} ->
      {{ Γ ⊢ A ≈ A' : Type@i }} ->
      {{ Γ ⊢ M : A' ® m ∈ El }}.
Proof.
  simpl.
  induction 1 using glu_univ_elem_ind; intros;
    simpl_glu_rel; repeat split; intros;
    destruct_by_head glu_bot; mauto 3.
  - firstorder.
  - econstructor; mauto 3.
  - destruct_by_head sigma_glu_exp_pred.
    econstructor; mauto 3.
  - econstructor; mauto 3.
    destruct_glu_eq; econstructor; mauto 3.
  - assert {{ Δ ⊢ A[σ] ≈ A'[σ] : Type@i[σ] }} as <-; mauto 4.
  - assert {{ Δ ⊢ A[σ] ≈ A'[σ] : Type@i }}; mauto 3.
Qed.

Add Parametric Morphism i P El a (H : glu_univ_elem i P El a) Γ : (El Γ)
    with signature wf_exp_eq Γ {{{Type@i}}} ==> eq ==> eq ==> iff as glu_univ_elem_trm_morphism_iff1.
Proof.
  split; intros;
    eapply glu_univ_elem_trm_resp_typ_exp_eq;
    mauto 2.
Qed.

Lemma glu_univ_elem_resp_ctx_eq : forall i P El a,
    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
    forall Γ Δ,
      {{ ⊢ Γ ≈ Δ }} ->
      (forall A, {{ Γ ⊢ A ® P }} -> {{ Δ ⊢ A ® P }}) /\
        (forall A M m, {{ Γ ⊢ M : A ® m ∈ El }} -> {{ Δ ⊢ M : A ® m ∈ El }}).
Proof.
  simpl.
  induction 1 using glu_univ_elem_ind; split; intros;
    simpl_glu_rel; mauto 2;
    repeat match goal with
      | H: glu_univ_elem _ ?P ?El _ |- _ =>
          assert ((forall A : typ, {{ Γ ⊢ A ® P }} -> {{ Δ ⊢ A ® P }}) /\ (forall A M m, {{ Γ ⊢ M : A ® m ∈ El }} -> {{ Δ ⊢ M : A ® m ∈ El }})) as [] by eauto 2;
          fail_if_dup
      end;
    econstructor; mauto 4.

  - split; mauto.
  - invert_per_univ_elems.
    destruct_rel_mod_eval.
    intuition.
  - destruct_glu_eq; econstructor; mauto 4.
  - split; mauto 4.
Qed.

Lemma glu_univ_elem_typ_resp_ctx_eq : forall i P El a,
    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
    forall Γ A Δ,
      {{ Γ ⊢ A ® P }} ->
      {{ ⊢ Γ ≈ Δ }} ->
      {{ Δ ⊢ A ® P }}.
Proof.
  intros; gen A;
  eapply proj1; eauto using glu_univ_elem_resp_ctx_eq.
Qed.

Add Parametric Morphism i P El a (H : glu_univ_elem i P El a) : P
    with signature wf_ctx_eq ==> eq ==> iff as glu_univ_elem_typ_morphism_iff2.
Proof.
  intros.
  split; intros;
    eapply glu_univ_elem_typ_resp_ctx_eq;
    mauto 2.
Qed.

Lemma glu_univ_elem_trm_resp_ctx_eq : forall i P El a,
    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
    forall Γ A M m Δ,
      {{ Γ ⊢ M : A ® m ∈ El }} ->
      {{ ⊢ Γ ≈ Δ }} ->
      {{ Δ ⊢ M : A ® m ∈ El }}.
Proof.
  intros; gen m M A;
  eapply proj2; eauto using glu_univ_elem_resp_ctx_eq.
Qed.

Add Parametric Morphism i P El a (H : glu_univ_elem i P El a) : El
    with signature wf_ctx_eq ==> eq ==> eq ==> eq ==> iff as glu_univ_elem_trm_morphism_iff2.
Proof.
  intros.
  split; intros;
    eapply glu_univ_elem_trm_resp_ctx_eq;
    mauto 2.
Qed.

Lemma glu_univ_elem_trm_escape : forall i P El a,
    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
    forall Γ M A m,
      {{ Γ ⊢ M : A ® m ∈ El }} ->
      {{ Γ ⊢ M : A }}.
Proof.
  simpl.
  induction 1 using glu_univ_elem_ind; intros;
    simpl_glu_rel; mauto 4.
Qed.

Lemma glu_univ_elem_per_univ : forall i P El a,
    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
    {{ Dom a ≈ a ∈ per_univ i }}.
Proof.
  simpl.
  induction 1 using glu_univ_elem_ind; intros; eexists;
    try solve [per_univ_elem_econstructor; mauto 3; try reflexivity].

  - subst. eapply per_univ_elem_core_univ'; trivial.
    reflexivity.
  - match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H).
    mauto.
  - match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H).
    per_univ_elem_econstructor; mauto.
Qed.

#[export]
Hint Resolve glu_univ_elem_per_univ : mctt.

Lemma glu_univ_elem_per_elem : forall i P El a,
    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
    forall Γ M A m R,
      {{ Γ ⊢ M : A ® m ∈ El }} ->
      {{ DF a ≈ a ∈ per_univ_elem i ↘ R }} ->
      {{ Dom m ≈ m ∈ R }}.
Proof.
  simpl.
  induction 1 using glu_univ_elem_ind; intros;
    match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem_nouip H);
    simpl_glu_rel;
    destruct_by_head glu_bot;
    try fold (per_univ j m m);
    mauto 4.

  - intros.
    destruct_rel_mod_app_nouip.
    destruct_rel_mod_eval_nouip.
    functional_eval_rewrite_clear.
    do_per_univ_elem_irrel_assert.
    econstructor; firstorder eauto.
  - destruct_by_head rel_mod_proj.
    destruct_rel_mod_eval_nouip.
    simplify_evals.
    functional_eval_rewrite_clear.
    do_per_univ_elem_irrel_assert.
    econstructor; firstorder eauto.
    intuition.
  - handle_per_univ_elem_irrel.
    pose proof (PER_refl1 _ R).
    destruct_glu_eq; destruct_by_head glu_bot; saturate_refl_for R; econstructor; mauto.
Qed.

Lemma glu_univ_elem_trm_typ : forall i P El a,
    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
    forall Γ M A m,
      {{ Γ ⊢ M : A ® m ∈ El }} ->
      {{ Γ ⊢ A ® P }}.
Proof.
  simpl.
  induction 1 using glu_univ_elem_ind; intros;
    simpl_glu_rel;
    mauto 4.

  econstructor; eauto.
  match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H).
  intros ? ? N n ? ? equiv_n.
  destruct_rel_mod_eval.
  enough (exists mn : domain, {{ $| m & n |↘ mn }} /\ {{ Δ ⊢ M[σ] N : OT[σ,,N] ® mn ∈ OEl n equiv_n }}) as [? []]; eauto 3.
Qed.

Lemma glu_univ_elem_trm_univ_lvl : forall i P El a,
    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
    forall Γ M A m,
      {{ Γ ⊢ M : A ® m ∈ El }} ->
      {{ Γ ⊢ A : Type@i }}.
Proof.
  intros.
  eapply glu_univ_elem_univ_lvl; [| eapply glu_univ_elem_trm_typ]; eassumption.
Qed.

Lemma glu_univ_elem_trm_resp_exp_eq : forall i P El a,
    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
    forall Γ A M m M',
      {{ Γ ⊢ M : A ® m ∈ El }} ->
      {{ Γ ⊢ M ≈ M' : A }} ->
      {{ Γ ⊢ M' : A ® m ∈ El }}.
Proof.
  simpl.
  induction 1 using glu_univ_elem_ind; intros;
    simpl_glu_rel;
    destruct_by_head glu_bot;
    repeat split; mauto 3.

  - repeat eexists; try split; eauto.
    eapply glu_univ_elem_typ_resp_exp_eq; mauto.

  - econstructor; eauto.
    match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H).
    intros.
    destruct_rel_mod_eval.
    assert {{ Δ ⊢ N : IT[σ] }} by eauto using glu_univ_elem_trm_escape.
    assert (exists mn : domain, {{ $| m & n |↘ mn }} /\ {{ Δ ⊢ M[σ] N : OT[σ,,N] ® mn ∈ OEl n equiv_n }}) as [? []] by intuition.
    eexists; split; eauto.
    enough {{ Δ ⊢ M[σ] N ≈ M'[σ] N : OT[σ,,N] }} by eauto.
    assert {{ Γ ⊢ M ≈ M' : Π IT OT }} as Hty by mauto.
    eassert {{ Δ ⊢ IT[σ] : Type@_ }} by mauto 3.
    eapply wf_exp_eq_sub_cong with (Γ := Δ) in Hty; [| eapply sub_eq_refl; mauto 3].
    autorewrite with mctt in Hty.
    eapply wf_exp_eq_app_cong with (N := N) (N' := N) in Hty; try pi_univ_level_tac; [|mauto 2].
    autorewrite with mctt in Hty.
    eassumption.
  - invert_per_univ_elem H3.
    eapply mk_sigma_glu_exp_pred with (equiv_m:=equiv_m); eauto.
    + eapply IHglu_univ_elem; mauto 3.
    + assert {{ Γ ⊢ (fst M) ≈ (fst M') : FT }} by mauto 3.
      assert {{ Γ ⊢s Id,,fst M : Γ , FT }} by (econstructor; mauto 4).
      assert {{ Γ ⊢ ST[Id,,(fst M)] ≈ ST[Id,,(fst M')] : Type@i }} by (eapply wf_exp_eq_conv'; [eapply wf_exp_eq_sub_cong |]; mauto 4).
      assert {{ Γ ⊢ snd M ≈ snd M' : ST[Id,,fst M] }} by (eapply wf_exp_eq_snd_cong with (A:=FT); mauto 3).
      destruct_rel_mod_eval.
      simplify_evals.
      eapply H2; mauto 3.
      eapply glu_univ_elem_trm_resp_typ_exp_eq; mauto 3.
  - econstructor; eauto.
    destruct_glu_eq; econstructor; mauto 3.
  - intros.
    enough {{ Δ ⊢ M[σ] ≈ M'[σ] : A[σ] }}; mauto 4.
Qed.

Add Parametric Morphism i P El a (H : glu_univ_elem i P El a) Γ T : (El Γ T)
    with signature wf_exp_eq Γ T ==> eq ==> iff as glu_univ_elem_trm_morphism_iff3.
Proof.
  split; intros;
    eapply glu_univ_elem_trm_resp_exp_eq;
    mauto 2.
Qed.

Lemma glu_univ_elem_core_univ' : forall j i typ_rel el_rel,
    j < i ->
    (typ_rel <∙> univ_glu_typ_pred j i) ->
    (el_rel <∙> univ_glu_exp_pred j i) ->
    {{ DG 𝕌@j ∈ glu_univ_elem i ↘ typ_rel ↘ el_rel }}.
Proof.
  intros.
  unshelve basic_glu_univ_elem_econstructor; mautosolve.
Qed.

#[export]
Hint Resolve glu_univ_elem_core_univ' : mctt.

Ltac glu_univ_elem_econstructor :=
  eapply glu_univ_elem_core_univ' + basic_glu_univ_elem_econstructor.

Lemma glu_univ_elem_univ_simple_constructor : forall {i},
    glu_univ_elem (S i) (univ_glu_typ_pred i (S i)) (univ_glu_exp_pred i (S i)) d{{{ 𝕌@i }}}.
Proof.
  intros.
  glu_univ_elem_econstructor; mauto; reflexivity.
Qed.

#[export]
Hint Resolve glu_univ_elem_univ_simple_constructor : mctt.

Ltac clear_predicate_equivalence :=
  repeat match goal with
    | H : ?R1 <∙> ?R2 |- _ =>
        (unify R1 R2; clear H) + (is_var R1; clear R1 H) + (is_var R2; clear R2 H)
    end.

Ltac rewrite_predicate_equivalence_left :=
  repeat match goal with
    | H : ?R1 <∙> ?R2 |- _ =>
        try setoid_rewrite H;
        (on_all_hyp: fun H' => assert_fails (unify H H'); unmark H; setoid_rewrite H in H');
        let T := type of H in
        fold (id T) in H;
        clear_predicate_equivalence
    end; unfold id in *.

Ltac rewrite_predicate_equivalence_right :=
  repeat match goal with
    | H : ?R1 <∙> ?R2 |- _ =>
        try setoid_rewrite <- H;
        (on_all_hyp: fun H' => assert_fails (unify H H'); unmark H; setoid_rewrite <- H in H');
        let T := type of H in
        fold (id T) in H;
        clear_predicate_equivalence
    end; unfold id in *.

Ltac apply_predicate_equivalence :=
  clear_predicate_equivalence;
  rewrite_predicate_equivalence_right;
  clear_predicate_equivalence;
  rewrite_predicate_equivalence_left;
  clear_predicate_equivalence.

Add Parametric Morphism i : (glu_univ_elem i)
    with signature glu_typ_pred_equivalence ==> glu_exp_pred_equivalence ==> eq ==> iff as simple_glu_univ_elem_morphism_iff.
Proof with mautosolve.
  intros P P' ? El El'.
  split; intro Horig; [gen El' P' | gen El P];
    induction Horig using glu_univ_elem_ind; unshelve glu_univ_elem_econstructor;
    try (etransitivity; [symmetry + idtac|]; eassumption); eauto.
Qed.

Add Parametric Morphism i : (neut_glu_typ_pred i)
    with signature per_bot ==> eq ==> eq ==> iff as neut_glu_typ_pred_morphism_iff.
Proof with mautosolve.
  split; intros []; econstructor; intuition;
    match_by_head per_bot ltac:(fun H => specialize (H (length Δ)) as [? []]);
    functional_read_rewrite_clear; intuition;
    match_by_head per_bot ltac:(fun H => rewrite H in *); eassumption.
Qed.

Add Parametric Morphism i : (neut_glu_typ_pred i)
    with signature per_bot ==> glu_typ_pred_equivalence as neut_glu_typ_pred_morphism_glu_typ_pred_equivalence.
Proof with mautosolve.
  split; apply neut_glu_typ_pred_morphism_iff; mauto.
Qed.

Add Parametric Morphism i : (neut_glu_exp_pred i)
    with signature per_bot ==> eq ==> eq ==> eq ==> eq ==> iff as neut_glu_exp_pred_morphism_iff.
Proof with mautosolve.
  split; intros []; econstructor; intuition;
    match_by_head per_bot ltac:(fun H => specialize (H (length Δ)) as [? []]);
    functional_read_rewrite_clear; intuition;
    match_by_head per_bot ltac:(fun H => rewrite H in *); eassumption.
Qed.

Add Parametric Morphism i : (neut_glu_exp_pred i)
    with signature per_bot ==> glu_exp_pred_equivalence as neut_glu_exp_pred_morphism_glu_exp_pred_equivalence.
Proof with mautosolve.
  split; apply neut_glu_exp_pred_morphism_iff; mauto.
Qed.

Add Parametric Morphism i IR : (pi_glu_typ_pred i IR)
    with signature glu_typ_pred_equivalence ==> glu_exp_pred_equivalence ==> eq ==> eq ==> eq ==> iff as pi_glu_typ_pred_morphism_iff.
Proof with mautosolve.
  split; intros []; econstructor; intuition.
Qed.

Add Parametric Morphism i IR : (pi_glu_typ_pred i IR)
    with signature glu_typ_pred_equivalence ==> glu_exp_pred_equivalence ==> eq ==> glu_typ_pred_equivalence as pi_glu_typ_pred_morphism_glu_typ_pred_equivalence.
Proof with mautosolve.
  split; intros []; econstructor; intuition.
Qed.

Add Parametric Morphism i IR : (pi_glu_exp_pred i IR)
    with signature glu_typ_pred_equivalence ==> glu_exp_pred_equivalence ==> relation_equivalence ==> eq ==> eq ==> eq ==> eq ==> eq ==> iff as pi_glu_exp_pred_morphism_iff.
Proof with mautosolve.
  split; intros []; econstructor; intuition.
Qed.

Add Parametric Morphism i IR : (pi_glu_exp_pred i IR)
    with signature glu_typ_pred_equivalence ==> glu_exp_pred_equivalence ==> relation_equivalence ==> eq ==> glu_exp_pred_equivalence as pi_glu_exp_pred_morphism_glu_exp_pred_equivalence.
Proof with mautosolve.
  split; intros []; econstructor; intuition.
Qed.

Add Parametric Morphism i FR : (sigma_glu_typ_pred i FR)
    with signature glu_typ_pred_equivalence ==> glu_exp_pred_equivalence ==> eq ==> eq ==> eq ==> iff as sigma_glu_typ_pred_morphism_iff.
Proof with mautosolve.
  split; intros []; econstructor; intuition.
Qed.

Add Parametric Morphism i FR : (sigma_glu_typ_pred i FR)
    with signature glu_typ_pred_equivalence ==> glu_exp_pred_equivalence ==> eq ==> glu_typ_pred_equivalence as sigma_glu_typ_pred_morphism_glu_typ_pred_equivalence.
Proof with mautosolve.
  split; intros []; econstructor; intuition.
Qed.

Add Parametric Morphism i FR : (sigma_glu_exp_pred i FR)
    with signature glu_typ_pred_equivalence ==> glu_exp_pred_equivalence ==> relation_equivalence ==> eq ==> eq ==> eq ==> eq ==> eq ==> eq ==> iff as sigma_glu_exp_pred_morphism_iff.
Proof with mautosolve.
  split; intros []; econstructor; intuition.
Qed.

Add Parametric Morphism i FR : (sigma_glu_exp_pred i FR)
    with signature glu_typ_pred_equivalence ==> glu_exp_pred_equivalence ==> relation_equivalence ==> eq ==> eq ==> glu_exp_pred_equivalence as sigma_glu_exp_pred_morphism_glu_exp_pred_equivalence.
Proof with mautosolve.
  split; intros []; econstructor; intuition.
Qed.

Add Parametric Morphism i m n : (eq_glu_typ_pred i m n)
    with signature glu_typ_pred_equivalence ==> glu_exp_pred_equivalence ==> eq ==> eq ==> iff as eq_glu_typ_pred_morphism_iff.
Proof with mautosolve.
  split; intros []; econstructor; intuition.
Qed.

Add Parametric Morphism i m n : (eq_glu_typ_pred i m n)
    with signature glu_typ_pred_equivalence ==> glu_exp_pred_equivalence ==> glu_typ_pred_equivalence as eq_glu_typ_pred_morphism_glu_typ_pred_equivalence.
Proof with mautosolve.
  split; intros []; econstructor; intuition.
Qed.

Add Parametric Morphism i m n IR : (eq_glu_exp_pred i m n IR)
    with signature glu_typ_pred_equivalence ==> glu_exp_pred_equivalence ==> eq ==> eq ==> eq ==> eq ==> iff as eq_glu_exp_pred_morphism_iff.
Proof with mautosolve.
  split; intros []; destruct_glu_eq; repeat (econstructor; intuition).
Qed.

Add Parametric Morphism i m n IR : (eq_glu_exp_pred i m n IR)
    with signature glu_typ_pred_equivalence ==> glu_exp_pred_equivalence ==> glu_exp_pred_equivalence as eq_glu_exp_pred_morphism_glu_exp_pred_equivalence.
Proof with mautosolve.
  split; intros []; destruct_glu_eq; repeat (econstructor; intuition).
Qed.

Lemma functional_glu_univ_elem : forall i a P P' El El',
    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
    {{ DG a ∈ glu_univ_elem i ↘ P' ↘ El' }} ->
    (P <∙> P') /\ (El <∙> El').
Proof.
  simpl.
  intros * Ha Ha'. gen P' El'.
  induction Ha using glu_univ_elem_ind; intros; basic_invert_glu_univ_elem Ha';
    apply_predicate_equivalence; try solve [split; reflexivity].
  - assert ((IP <∙> IP0) /\ (IEl <∙> IEl0)) as [] by mauto.
    apply_predicate_equivalence.
    handle_per_univ_elem_irrel.
    (on_all_hyp: fun H => directed invert_per_univ_elem H).
    handle_per_univ_elem_irrel.
    split; [intros Γ C | intros Γ M C m].
    + split; intros []; econstructor; intuition;
        [ rename equiv_m into equiv0_m; assert (equiv_m : in_rel m m) by intuition
        | assert (equiv0_m : in_rel0 m m) by intuition ];
        destruct_rel_mod_eval;
        functional_eval_rewrite_clear;
        assert ((OP m equiv_m <∙> OP0 m equiv0_m) /\ (OEl m equiv_m <∙> OEl0 m equiv0_m)) as [] by mauto 3;
        intuition.
    + split; intros []; econstructor; intuition;
        [ rename equiv_n into equiv0_n; assert (equiv_n : in_rel n n) by intuition
        | assert (equiv0_n : in_rel0 n n) by intuition];
        destruct_rel_mod_eval;
        [ assert (exists m0n, {{ $| m0 & n |↘ m0n }} /\ {{ Δ ⊢ M0[σ] N : OT[σ,,N] ® m0n ∈ OEl n equiv_n }}) by intuition
        | assert (exists m0n, {{ $| m0 & n |↘ m0n }} /\ {{ Δ ⊢ M0[σ] N : OT[σ,,N] ® m0n ∈ OEl0 n equiv0_n }}) by intuition];
        destruct_conjs;
        assert ((OP n equiv_n <∙> OP0 n equiv0_n) /\ (OEl n equiv_n <∙> OEl0 n equiv0_n)) as [] by mauto 3;
        eexists; split; intuition.
  - assert ((FP <∙> FP0) /\ (FEl <∙> FEl0)) as [] by mauto.
    apply_predicate_equivalence.
    handle_per_univ_elem_irrel.
    (on_all_hyp: fun H => directed invert_per_univ_elem H).
    handle_per_univ_elem_irrel.
    split; [intros Γ C | intros Γ M C m].
    + split; intros []; econstructor; intuition;
        [ rename equiv_m into equiv0_m; assert (equiv_m : fst_rel m m) by intuition
        | assert (equiv0_m : fst_rel0 m m) by intuition];
        destruct_rel_mod_eval;
        functional_eval_rewrite_clear;
        assert ((SP m equiv_m <∙> SP0 m equiv0_m) /\ (SEl m equiv_m <∙> SEl0 m equiv0_m)) as [] by mauto 3;
        intuition.
    + split; intros [];
        [ assert (equiv0_m : fst_rel0 m1 m1) by intuition
        | rename equiv_m into equiv0_m; assert (equiv_m : fst_rel m1 m1) by intuition];
        destruct_rel_mod_eval;
        assert ((SP m1 equiv_m <∙> SP0 m1 equiv0_m) /\ (SEl m1 equiv_m <∙> SEl0 m1 equiv0_m)) as [] by mauto 3;
        [> econstructor; mauto 3; [| intuition] ..];
        intros;
        [ rename equiv_m' into equiv0_m'; assert (equiv_m' : fst_rel m' m') by intuition
        | assert (equiv0_m' : fst_rel0 m' m') by intuition];
        destruct_rel_mod_eval;
        assert ((SP m' equiv_m' <∙> SP0 m' equiv0_m') /\ (SEl m' equiv_m' <∙> SEl0 m' equiv0_m')) as [] by mauto 3;
        intuition.
  - assert ((P <∙> P0) /\ (El <∙> El0)) as [] by mauto.
    apply_predicate_equivalence.
    handle_per_univ_elem_irrel.
    split; [intros Γ C | intros Γ M C m'];
      split; intros []; econstructor; intuition;
      destruct_glu_eq;
      econstructor; intros; apply_equiv_right; mauto 4.
Qed.

Ltac apply_functional_glu_univ_elem1 :=
  let tactic_error o1 o2 := fail 2 "functional_glu_univ_elem biconditional between" o1 "and" o2 "cannot be solved" in
  match goal with
  | H1 : {{ DG ^?a ∈ glu_univ_elem ?i ↘ ?P1 ↘ ?El1 }},
      H2 : {{ DG ^?a ∈ glu_univ_elem ?i' ↘ ?P2 ↘ ?El2 }} |- _ =>
      unify i i';
      assert_fails (unify P1 P2; unify El1 El2);
      match goal with
      | H : P1 <∙> P2, H0 : El1 <∙> El2 |- _ => fail 1
      | H : P1 <∙> P2, H0 : El2 <∙> El1 |- _ => fail 1
      | H : P2 <∙> P1, H0 : El1 <∙> El2 |- _ => fail 1
      | H : P2 <∙> P1, H0 : El2 <∙> El1 |- _ => fail 1
      | _ => assert ((P1 <∙> P2) /\ (El1 <∙> El2)) as [] by (eapply functional_glu_univ_elem; [apply H1 | apply H2]) || tactic_error P1 P2
      end
  end.

Ltac apply_functional_glu_univ_elem :=
  repeat apply_functional_glu_univ_elem1.

Ltac handle_functional_glu_univ_elem :=
  functional_eval_rewrite_clear;
  fold glu_typ_pred in *;
  fold glu_exp_pred in *;
  apply_functional_glu_univ_elem;
  apply_predicate_equivalence;
  clear_dups.

Lemma glu_univ_elem_pi_clean_inversion1 : forall {i a ρ B in_rel P El},
  {{ DF a ≈ a ∈ per_univ_elem i ↘ in_rel }} ->
  {{ DG Π a ρ B ∈ glu_univ_elem i ↘ P ↘ El }} ->
  exists IP IEl (OP : forall c (equiv_c_c : {{ Dom c ≈ c ∈ in_rel }}), glu_typ_pred)
     (OEl : forall c (equiv_c_c : {{ Dom c ≈ c ∈ in_rel }}), glu_exp_pred) elem_rel,
      {{ DG a ∈ glu_univ_elem i ↘ IP ↘ IEl }} /\
        (forall c (equiv_c : {{ Dom c ≈ c ∈ in_rel }}) b,
            {{ ⟦ B ⟧ ρ ↦ c ↘ b }} ->
            {{ DG b ∈ glu_univ_elem i ↘ OP _ equiv_c ↘ OEl _ equiv_c }}) /\
        {{ DF Π a ρ B ≈ Π a ρ B ∈ per_univ_elem i ↘ elem_rel }} /\
        (P <∙> pi_glu_typ_pred i in_rel IP IEl OP) /\
        (El <∙> pi_glu_exp_pred i in_rel IP IEl elem_rel OEl).
Proof.
  intros *.
  simpl.
  intros Hinper Hglu.
  basic_invert_glu_univ_elem Hglu.
  handle_functional_glu_univ_elem.
  handle_per_univ_elem_irrel.
  do 5 eexists.
  repeat split.
  1,3: eassumption.
  1: instantiate (1 := fun c equiv_c Γ A M m => forall (b : domain) Pb Elb,
                          {{ ⟦ B ⟧ ρ ↦ c ↘ b }} ->
                          {{ DG b ∈ glu_univ_elem i ↘ Pb ↘ Elb }} ->
                          {{ Γ ⊢ M : A ® m ∈ Elb }}).
  1: instantiate (1 := fun c equiv_c Γ A => forall (b : domain) Pb Elb,
                          {{ ⟦ B ⟧ ρ ↦ c ↘ b }} ->
                          {{ DG b ∈ glu_univ_elem i ↘ Pb ↘ Elb }} ->
                          {{ Γ ⊢ A ® Pb }}).
  2-5: intros []; econstructor; mauto.
  all: intros.
  - assert {{ Dom c ≈ c ∈ in_rel0 }} as equiv0_c by intuition.
    assert {{ DG b ∈ glu_univ_elem i ↘ OP c equiv0_c ↘ OEl c equiv0_c }} by mauto 3.
    apply -> simple_glu_univ_elem_morphism_iff; [| reflexivity | |]; [eauto | |].
    + intros ? **.
      split; intros; handle_functional_glu_univ_elem; intuition.
    + intros ? **.
      split; [intros; handle_functional_glu_univ_elem |]; intuition.
  - assert {{ Dom m ≈ m ∈ in_rel0 }} as equiv0_m by intuition.
    assert {{ DG b ∈ glu_univ_elem i ↘ OP m equiv0_m ↘ OEl m equiv0_m }} by mauto 3.
    handle_functional_glu_univ_elem.
    intuition.
  - match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H).
    destruct_rel_mod_eval.
    intuition.
  - assert {{ Dom n ≈ n ∈ in_rel0 }} as equiv0_n by intuition.
    assert (exists mn : domain, {{ $| m & n |↘ mn }} /\ {{ Δ ⊢ M[σ] N : OT[σ,,N] ® mn ∈ OEl n equiv0_n }}) by mauto 3.
    destruct_conjs.
    eexists.
    intuition.
    assert {{ DG b ∈ glu_univ_elem i ↘ OP n equiv0_n ↘ OEl n equiv0_n }} by mauto 3.
    handle_functional_glu_univ_elem.
    intuition.
  - assert (exists mn : domain,
               {{ $| m & n |↘ mn }} /\
                 (forall (b : domain) (Pb : glu_typ_pred) (Elb : glu_exp_pred),
                     {{ ⟦ B ⟧ ρ ↦ n ↘ b }} ->
                     {{ DG b ∈ glu_univ_elem i ↘ Pb ↘ Elb }} ->
                     {{ Δ ⊢ M[σ] N : OT[σ,,N] ® mn ∈ Elb }})) by intuition.
    destruct_conjs.
    match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H).
    handle_per_univ_elem_irrel.
    destruct_rel_mod_eval.
    destruct_rel_mod_app.
    functional_eval_rewrite_clear.
    eexists.
    intuition.
Qed.

Lemma glu_univ_elem_pi_clean_inversion2 : forall {i a ρ B in_rel IP IEl P El},
  {{ DF a ≈ a ∈ per_univ_elem i ↘ in_rel }} ->
  {{ DG a ∈ glu_univ_elem i ↘ IP ↘ IEl }} ->
  {{ DG Π a ρ B ∈ glu_univ_elem i ↘ P ↘ El }} ->
  exists (OP : forall c (equiv_c_c : {{ Dom c ≈ c ∈ in_rel }}), glu_typ_pred)
     (OEl : forall c (equiv_c_c : {{ Dom c ≈ c ∈ in_rel }}), glu_exp_pred) elem_rel,
    (forall c (equiv_c : {{ Dom c ≈ c ∈ in_rel }}) b,
        {{ ⟦ B ⟧ ρ ↦ c ↘ b }} ->
        {{ DG b ∈ glu_univ_elem i ↘ OP _ equiv_c ↘ OEl _ equiv_c }}) /\
      {{ DF Π a ρ B ≈ Π a ρ B ∈ per_univ_elem i ↘ elem_rel }} /\
      (P <∙> pi_glu_typ_pred i in_rel IP IEl OP) /\
      (El <∙> pi_glu_exp_pred i in_rel IP IEl elem_rel OEl).
Proof.
  intros *.
  simpl.
  intros Hinper Hinglu Hglu.
  unshelve eapply (glu_univ_elem_pi_clean_inversion1 _) in Hglu; shelve_unifiable; [eassumption |];
    destruct Hglu as [? [? [? [? [? [? [? [? []]]]]]]]].
  handle_functional_glu_univ_elem.
  do 3 eexists.
  repeat split; try eassumption;
    intros []; econstructor; mauto.
Qed.

Lemma glu_univ_elem_sigma_clean_inversion1 : forall {i a ρ B fst_rel P El},
  {{ DF a ≈ a ∈ per_univ_elem i ↘ fst_rel }} ->
  {{ DG Σ a ρ B ∈ glu_univ_elem i ↘ P ↘ El }} ->
  exists FP FEl (SP : forall c (equiv_c_c : {{ Dom c ≈ c ∈ fst_rel }}), glu_typ_pred)
     (SEl : forall c (equiv_c_c : {{ Dom c ≈ c ∈ fst_rel }}), glu_exp_pred) elem_rel,
      {{ DG a ∈ glu_univ_elem i ↘ FP ↘ FEl }} /\
        (forall c (equiv_c : {{ Dom c ≈ c ∈ fst_rel }}) b,
            {{ ⟦ B ⟧ ρ ↦ c ↘ b }} ->
            {{ DG b ∈ glu_univ_elem i ↘ SP _ equiv_c ↘ SEl _ equiv_c }}) /\
        {{ DF Σ a ρ B ≈ Σ a ρ B ∈ per_univ_elem i ↘ elem_rel }} /\
        (P <∙> sigma_glu_typ_pred i fst_rel FP FEl SP) /\
        (El <∙> sigma_glu_exp_pred i fst_rel FP FEl elem_rel SP SEl).
Proof.
    intros *.
  simpl.
  intros Hinper Hglu.
  basic_invert_glu_univ_elem Hglu.
  handle_functional_glu_univ_elem.
  handle_per_univ_elem_irrel.
  do 5 eexists.
  repeat split; eauto.
  (* How these are come up with? *)
  1: instantiate (1 := fun c equiv_c Γ A M m => forall (b : domain) Pb Elb,
                          {{ ⟦ B ⟧ ρ ↦ c ↘ b }} ->
                          {{ DG b ∈ glu_univ_elem i ↘ Pb ↘ Elb }} ->
                          {{ Γ ⊢ M : A ® m ∈ Elb }}).
  1: instantiate (1 := fun c equiv_c Γ A => forall (b : domain) Pb Elb,
                          {{ ⟦ B ⟧ ρ ↦ c ↘ b }} ->
                          {{ DG b ∈ glu_univ_elem i ↘ Pb ↘ Elb }} ->
                          {{ Γ ⊢ A ® Pb }}).
  - intros. assert {{ Dom c ≈ c ∈ fst_rel0 }} as equiv0_c by intuition.
    assert {{ DG b ∈ glu_univ_elem i ↘ SP c equiv0_c ↘ SEl c equiv0_c }} by mauto 3.
    apply -> simple_glu_univ_elem_morphism_iff; [| reflexivity | |]; [eauto | |].
    + intros ? ? ? ?.
      split; intros; handle_functional_glu_univ_elem; intuition.
    + intros ? ?.
      split; [intros; handle_functional_glu_univ_elem |]; intuition.
  - intros []; econstructor; mauto; intuition.
    assert {{ Dom m ≈ m ∈ fst_rel0 }} as equiv0_m by intuition.
    assert {{ DG b ∈ glu_univ_elem i ↘ SP m equiv0_m ↘ SEl m equiv0_m }} by mauto 3.
    handle_functional_glu_univ_elem.
    intuition.
  - intros.
    dependent destruction H4.
    match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H).
    apply_relation_equivalence.
    econstructor; mauto 3. intros.
    destruct_rel_mod_eval. simplify_evals.
    intuition.
  - intros [].
    econstructor; mauto 3; intuition.
    + assert {{ Dom m' ≈ m' ∈ fst_rel0 }} as equiv0_m' by intuition;
      assert {{ DG b ∈ glu_univ_elem i ↘ SP m' equiv0_m' ↘ SEl m' equiv0_m' }} by mauto 3.
      handle_functional_glu_univ_elem.
      intuition.
    + assert {{ DG b ∈ glu_univ_elem i ↘ SP m1 equiv_m ↘ SEl m1 equiv_m }} by mauto 3.
      handle_functional_glu_univ_elem.
      intuition.
  - intros [].
    match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H).
    assert (equiv0_m : {{ Dom m1 ≈ m1 ∈ fst_rel0 }}) by intuition.
    eapply mk_sigma_glu_exp_pred with (equiv_m:=equiv0_m); intuition;
    destruct_rel_mod_eval; simplify_evals; intuition.
Qed.

Lemma glu_univ_elem_sigma_clean_inversion2 : forall {i a ρ B fst_rel FP FEl P El},
  {{ DF a ≈ a ∈ per_univ_elem i ↘ fst_rel }} ->
  {{ DG a ∈ glu_univ_elem i ↘ FP ↘ FEl }} ->
  {{ DG Σ a ρ B ∈ glu_univ_elem i ↘ P ↘ El }} ->
  exists (SP : forall c (equiv_c_c : {{ Dom c ≈ c ∈ fst_rel }}), glu_typ_pred)
     (SEl : forall c (equiv_c_c : {{ Dom c ≈ c ∈ fst_rel }}), glu_exp_pred) elem_rel,
        (forall c (equiv_c : {{ Dom c ≈ c ∈ fst_rel }}) b,
            {{ ⟦ B ⟧ ρ ↦ c ↘ b }} ->
            {{ DG b ∈ glu_univ_elem i ↘ SP _ equiv_c ↘ SEl _ equiv_c }}) /\
        {{ DF Σ a ρ B ≈ Σ a ρ B ∈ per_univ_elem i ↘ elem_rel }} /\
        (P <∙> sigma_glu_typ_pred i fst_rel FP FEl SP) /\
        (El <∙> sigma_glu_exp_pred i fst_rel FP FEl elem_rel SP SEl).
Proof.
  intros *.
  simpl.
  intros Hinper Hinglu Hglu.
  unshelve eapply (glu_univ_elem_sigma_clean_inversion1 _) in Hglu; shelve_unifiable; [eassumption |];
    destruct Hglu as [? [? [? [? [? [? [? [? []]]]]]]]];
  match_by_head per_univ_elem ltac:(fun H => directed invert_per_univ_elem H).
  handle_functional_glu_univ_elem.
  do 3 eexists.
  repeat split; try eassumption; handle_functional_glu_univ_elem.
  1: per_univ_elem_econstructor; eauto.
  all: intros []; econstructor; mauto;
    intros; handle_functional_glu_univ_elem; auto.
Qed.

Ltac invert_glu_univ_elem H :=
  (unshelve eapply (glu_univ_elem_pi_clean_inversion2 _ _) in H; shelve_unifiable; [eassumption | eassumption |];
   deex_in H; destruct H as [? [? []]])
  + (unshelve eapply (glu_univ_elem_pi_clean_inversion1 _) in H; shelve_unifiable; [eassumption |];
   deex_in H; destruct H as [? [? [? []]]])
  + (unshelve eapply (glu_univ_elem_sigma_clean_inversion2 _ _) in H; shelve_unifiable; [eassumption | eassumption |];
   deex_in H; destruct H as [? [? []]])
  + (unshelve eapply (glu_univ_elem_sigma_clean_inversion1 _) in H; shelve_unifiable; [eassumption |];
   deex_in H; destruct H as [? [? [? []]]])
  + basic_invert_glu_univ_elem H.

(* TODO: unify with the uip version above *)
Ltac invert_glu_univ_elem_nouip H :=
  (unshelve eapply (glu_univ_elem_pi_clean_inversion2 _ _) in H; shelve_unifiable; [eassumption | eassumption |];
   destruct H as [? [? [? [? [? []]]]]])
  + (unshelve eapply (glu_univ_elem_pi_clean_inversion1 _) in H; shelve_unifiable; [eassumption |];
   destruct H as [? [? [? [? [? [? [? [? []]]]]]]]])
  + (unshelve eapply (glu_univ_elem_sigma_clean_inversion2 _ _) in H; shelve_unifiable; [eassumption | eassumption |];
   destruct H as [? [? [? [? [? []]]]]])
  + (unshelve eapply (glu_univ_elem_sigma_clean_inversion1 _) in H; shelve_unifiable; [eassumption |];
   destruct H as [? [? [? [? [? [? [? [? []]]]]]]]])
  + basic_invert_glu_univ_elem_nouip H.

#[local]
Ltac resp_per_IH :=
  match_by_head1 glu_univ_elem
    ltac:(fun H =>
            match goal with
            | H' : _ |- _ => eapply H' in H
            end);
  eauto; intuition.

Lemma glu_univ_elem_resp_per_univ_elem : forall i a a' R,
    {{ DF a ≈ a' ∈ per_univ_elem i ↘ R }} ->
    forall P El,
    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
    {{ DG a' ∈ glu_univ_elem i ↘ P ↘ El }} /\
      (forall Γ M A m m',
          {{ Γ ⊢ M : A ® m ∈ El }} ->
          {{ Dom m ≈ m' ∈ R }} ->
          {{ Γ ⊢ M : A ® m' ∈ El }}).
Proof.
  simpl.
  intros * Hper * Horig.
  pose proof Hper.
  gen P El.

  induction Hper using per_univ_elem_ind; intros; subst;
    saturate_refl_for per_univ_elem;
    invert_glu_univ_elem Horig.

  1-6:
    split; [glu_univ_elem_econstructor | intros];
    try eassumption; mauto 3;
    intros;
    handle_per_univ_elem_irrel;
    handle_functional_glu_univ_elem;
    simpl in *;
    destruct_all;
    mauto 3.

  - repeat split; eauto.
    resp_per_IH.
    mauto.
  - resp_per_IH.
  - invert_per_univ_elem H.
    destruct_rel_mod_eval.
    handle_per_univ_elem_irrel.
    eassert {{ DG ^_ ∈ glu_univ_elem i ↘ OP c equiv_c ↘ OEl c equiv_c }} by eauto 2.
    resp_per_IH.
  - simpl_glu_rel.
    invert_per_univ_elem H10.

    econstructor; mauto 3.
    + eapply H17.
      pose proof (proj1 (H17 _ _) H16).
      simpl in *.

      intros.
      saturate_refl_for in_rel.
      pose proof (H18 _ _ equiv_c_c') as [].
      pose proof (H18 _ _ H19) as [].
      pose proof (H10 _ _ equiv_c_c') as [].
      pose proof (H10 _ _ H19) as [].
      simplify_evals.
      econstructor; eauto.
      symmetry.
      etransitivity.
      * symmetry. eassumption.
      * handle_per_univ_elem_irrel.
        eapply H24.
        eassumption.
    + resp_per_IH.
      destruct_rel_mod_eval.
      handle_per_univ_elem_irrel.
      pose proof (H9 _ equiv_n _ H22).
      eapply H28 in H25 as []; eauto.
      destruct (H15 _ _ _ _ H20 H21 equiv_n) as [? []].
      destruct (H16 _ _ equiv_n) as [].
      simplify_evals.
      eauto.
  - resp_per_IH.
  - resp_per_IH.
    destruct_rel_mod_eval.
    simplify_evals.
    eapply proj1, H15; mauto 3.
  - simpl_glu_rel.
    destruct_by_head rel_mod_proj.
    simplify_evals.
    match goal with
    | _: {{ π₁ m ↘ ^?m1' }},
        _: {{ π₂ m ↘ ^?m2' }},
          _: {{ π₁ m' ↘ ^?m1'' }},
            _: {{ π₂ m' ↘ ^?m2'' }},
              _: SEl ?m1' ?equiv Γ {{{ ST[Id,,fst M] }}} {{{ snd M }}} ?m2' |- _ =>
        rename equiv into equiv_m1;
        rename m1' into m1;
        rename m2' into m2;
        rename m1'' into m'1;
        rename m2'' into m'2
    end.
    assert (fst_rel m'1 m'1) as equiv_m'1 by (etransitivity; [symmetry |]; eassumption).
    econstructor; intuition;
      destruct_rel_mod_eval;
      handle_per_univ_elem_irrel;
      simplify_evals;
      match goal with
      | _: {{ ⟦ B ⟧ ρ ↦ m1 ↘ ^?a }},
          _: {{ ⟦ B' ⟧ ρ' ↦ m1 ↘ ^?a' }},
            _: {{ ⟦ B ⟧ ρ ↦ m'1 ↘ ^?a'' }},
              _: {{ ⟦ B' ⟧ ρ' ↦ m'1 ↘ ^?a''' }} |- _ =>
          rename a into b;
          rename a' into b';
          rename a'' into b0;
          rename a''' into b'0
      end;
      assert {{ DG b ∈ glu_univ_elem i ↘ SP _ equiv_m1 ↘ SEl _ equiv_m1 }} by eauto;
      assert {{ DG b0 ∈ glu_univ_elem i ↘ SP _ equiv_m'1 ↘ SEl _ equiv_m'1 }} by eauto;
      assert {{ DG b'0 ∈ glu_univ_elem i ↘ SP _ equiv_m1 ↘ SEl _ equiv_m1 }} by (eapply proj1; eauto);
      assert {{ DG b'0 ∈ glu_univ_elem i ↘ SP _ equiv_m'1 ↘ SEl _ equiv_m'1 }} by (eapply proj1; eauto);
      handle_functional_glu_univ_elem.
    * econstructor; mauto 3.
      eapply H33; etransitivity; [symmetry |]; apply H32; eassumption.
    * eapply H39, H35; mauto 3; eapply H28, H32; eassumption.
  - resp_per_IH.
  - pose proof (PER_refl2 _ R). mauto.
  - pose proof (PER_refl2 _ R). mauto.
  - split; intros []; econstructor; intuition.
  - split; intros []; econstructor; intuition;
      destruct_glu_eq;
      econstructor; mauto 3;
      apply_equiv_left.
    + etransitivity; eauto.
      symmetry. trivial.
    + etransitivity; eauto.
    + etransitivity; [| eauto]; eauto.
    + etransitivity; eauto.
      symmetry. trivial.
  - simpl_glu_rel.
    econstructor; eauto.
    destruct_glu_eq; match_by_head1 per_eq progressive_invert; econstructor; mauto 3; intros.
    + etransitivity; mauto.
    + etransitivity; eauto.
      symmetry. eauto.
    + resp_per_IH.
  - apply neut_glu_typ_pred_morphism_glu_typ_pred_equivalence.
    eassumption.
  - apply neut_glu_exp_pred_morphism_glu_exp_pred_equivalence.
    eassumption.
  - simpl_glu_rel.
    progressive_inversion.
    econstructor; unfold neut_glu_typ_pred; mauto 3.
Qed.

Lemma glu_univ_elem_resp_per_univ : forall i a a' P El,
    {{ Dom a ≈ a' ∈ per_univ i }} ->
    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
    {{ DG a' ∈ glu_univ_elem i ↘ P ↘ El }}.
Proof.
  intros * [? H] ?.
  eapply glu_univ_elem_resp_per_univ_elem in H; eauto.
  intuition.
Qed.

Lemma glu_univ_elem_resp_per_elem : forall i a a' R P El Γ M A m m',
    {{ DF a ≈ a' ∈ per_univ_elem i ↘ R }} ->
    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
    {{ Γ ⊢ M : A ® m ∈ El }} ->
    {{ Dom m ≈ m' ∈ R }} ->
    {{ Γ ⊢ M : A ® m' ∈ El }}.
Proof.
  intros * H ?.
  eapply glu_univ_elem_resp_per_univ_elem in H; eauto.
  intuition.
Qed.