Mcltt.Core.Soundness.NatCases

From Coq Require Import Morphisms Morphisms_Prop Morphisms_Relations Relation_Definitions RelationClasses SetoidTactics.

From Mcltt Require Import Base LibTactics.
From Mcltt.Core.Completeness Require Import FundamentalTheorem.
From Mcltt.Core.Semantic Require Import Realizability.
From Mcltt.Core.Soundness Require Import ContextCases LogicalRelation Realizability SubstitutionCases SubtypingCases TermStructureCases UniverseCases.
From Mcltt.Core.Syntactic Require Import Corollaries.
Import Domain_Notations.

Lemma glu_rel_exp_nat : forall {Γ i},
    {{ ⊩ Γ }} ->
    {{ Γ ⊩ ℕ : Type@i }}.
Proof.
  intros * [Sb].
  assert {{ ⊢ Γ }} by mauto.
  eapply glu_rel_exp_of_typ; mauto 3.
  intros.
  assert {{ Δ ⊢s σ : Γ }} by mauto 3.
  split; mauto 3.
  eexists; repeat split; mauto 3.
  - eexists; per_univ_elem_econstructor; reflexivity.
  - intros.
    match_by_head1 glu_univ_elem invert_glu_univ_elem.
    apply_predicate_equivalence.
    unfold nat_glu_typ_pred.
    mauto 3.
Qed.

#[export]
Hint Resolve glu_rel_exp_nat : mcltt.

Lemma glu_rel_exp_sub_nat : forall {Γ σ Δ M},
    {{ Γ ⊩s σ : Δ }} ->
    {{ Δ ⊩ M : ℕ }} ->
    {{ Γ ⊩ M[σ] : ℕ }}.
Proof.
  intros.
  assert {{ Γ ⊢s σ : Δ }} by mauto 3.
  assert {{ Γ ⊢ ℕ[σ] ⊆ ℕ }} by mautosolve 3.
  assert {{ Γ ⊩ M[σ] : ℕ[σ] }} by mauto 3.
  mautosolve 4.
Qed.

#[export]
Hint Resolve glu_rel_exp_sub_nat : mcltt.

Lemma glu_rel_exp_clean_inversion2'' : forall {Γ Sb M},
    {{ EG Γ ∈ glu_ctx_env ↘ Sb }} ->
    {{ Γ ⊩ M : ℕ }} ->
    glu_rel_exp_clean_inversion2_result 0 Sb M {{{ ℕ }}}.
Proof.
  intros * ? HM.
  assert {{ Γ ⊩ ℕ : Type@0 }} by mauto 3.
  eapply glu_rel_exp_clean_inversion2 in HM; mauto 3.
Qed.

Ltac invert_glu_rel_exp H ::=
  (unshelve eapply (glu_rel_exp_clean_inversion2'' _) in H; shelve_unifiable; [eassumption |];
   unfold glu_rel_exp_clean_inversion2_result in H)
  + (unshelve eapply (glu_rel_exp_clean_inversion2' _) in H; shelve_unifiable; [eassumption |];
     unfold glu_rel_exp_clean_inversion2_result in H)
  + (unshelve eapply (glu_rel_exp_clean_inversion2 _ _) in H; shelve_unifiable; [eassumption | eassumption |];
     unfold glu_rel_exp_clean_inversion2_result in H)
  + (unshelve eapply (glu_rel_exp_clean_inversion1 _) in H; shelve_unifiable; [eassumption |];
     destruct H as [])
  + (inversion H; subst).

Lemma glu_rel_exp_of_nat : forall {Γ Sb M},
    {{ EG Γ ∈ glu_ctx_env ↘ Sb }} ->
    (forall Δ σ ρ, {{ Δ ⊢s σ ® ρ ∈ Sb }} -> exists m, {{ ⟦ M ⟧ ρ ↘ m }} /\ glu_nat Δ {{{ M[σ] }}} m) ->
    {{ Γ ⊩ M : ℕ }}.
Proof.
  intros * ? Hbody.
  eexists; split; mauto 3.
  exists 0.
  intros.
  edestruct Hbody as [? []]; mauto 3.
  econstructor; mauto 3.
  - glu_univ_elem_econstructor; mauto 3; reflexivity.
  - simpl; split; mauto 3.
Qed.

Lemma glu_rel_exp_zero : forall {Γ},
    {{ ⊩ Γ }} ->
    {{ Γ ⊩ zero : ℕ }}.
Proof.
  intros * [Sb].
  eapply glu_rel_exp_of_nat; mauto 3.
  intros.
  eexists; split; mauto 4.
Qed.

#[export]
Hint Resolve glu_rel_exp_zero : mcltt.

Lemma glu_rel_exp_succ : forall {Γ M},
    {{ Γ ⊩ M : ℕ }} ->
    {{ Γ ⊩ succ M : ℕ }}.
Proof.
  intros * HM.
  assert {{ ⊩ Γ }} as [SbΓ] by mauto 3.
  assert {{ Γ ⊢ M : ℕ }} by mauto 3.
  invert_glu_rel_exp HM.
  eapply glu_rel_exp_of_nat; mauto.
  intros.
  destruct_glu_rel_exp_with_sub.
  simplify_evals.
  match_by_head1 glu_univ_elem invert_glu_univ_elem.
  apply_predicate_equivalence.
  inversion_clear_by_head nat_glu_exp_pred.
  eexists; split; mauto 3.
  econstructor; mauto.
Qed.

#[export]
Hint Resolve glu_rel_exp_succ : mcltt.

Lemma glu_rel_sub_extend_nat : forall {Γ σ Δ M},
    {{ Γ ⊩s σ : Δ }} ->
    {{ Γ ⊩ M : ℕ }} ->
    {{ Γ ⊩s σ,,M : Δ, ℕ }}.
Proof.
  intros.
  assert {{ ⊩ Δ }} by mauto 2.
  assert {{ Γ ⊩ ℕ[σ] : Type@0 }} by mauto 3.
  assert {{ Γ ⊢s σ : Δ }} by mauto 3.
  assert {{ Γ ⊢ ℕ ⊆ ℕ[σ] }} by mautosolve 4.
  assert {{ Γ ⊩ M : ℕ[σ] }}; mautosolve 3.
Qed.

#[export]
Hint Resolve glu_rel_sub_extend_nat : mcltt.

Lemma glu_rel_exp_natrec_zero_helper : forall {i Γ SbΓ A MZ MS Δ M σ ρ am P El},
    {{ EG Γ ∈ glu_ctx_env ↘ SbΓ }} ->
    {{ Γ, ℕ ⊢ A : Type@i }} ->
    {{ Γ ⊩ A[Id,,zero] : Type@i }} ->
    {{ Γ ⊩ MZ : A[Id,,zero] }} ->
    {{ Γ, ℕ, A ⊢ MS : A[Wk∘Wk,,succ #1] }} ->
    {{ Δ ⊢ M ≈ zero : ℕ }} ->
    {{ Δ ⊢s σ ® ρ ∈ SbΓ }} ->
    {{ ⟦ A ⟧ ρ ↦ zero ↘ am }} ->
    {{ DG am ∈ glu_univ_elem i ↘ P ↘ El }} ->
    exists r,
      {{ rec zero ⟦return A | zero -> MZ | succ -> MS end⟧ ρ ↘ r }} /\
        {{ Δ ⊢ rec M return A[q σ] | zero -> MZ[σ] | succ -> MS[q (q σ)] end : A[σ,,M] ® r ∈ El }}.
Proof.
  intros * ? ? ? HMZ **.
  assert {{ Γ ⊢ MZ : A[Id,,zero] }} by mauto 3.
  invert_glu_rel_exp HMZ.
  assert {{ Γ ⊩ ℕ : Type@i }} as Hℕ by mauto 3.
  pose (SbΓℕ := cons_glu_sub_pred i Γ {{{ ℕ }}} SbΓ).
  assert {{ EG Γ, ℕ ∈ glu_ctx_env ↘ SbΓℕ }} by (invert_glu_rel_exp Hℕ; econstructor; mauto 3; reflexivity).
  destruct_glu_rel_exp_with_sub.
  simplify_evals.
  rename m into mz.
  eexists mz; split; mauto 3.
  handle_functional_glu_univ_elem.
  assert {{ Δ ⊢s σ : Γ }} by mauto 2.
  assert {{ ⊢ Δ }} by mauto 2.
  assert {{ ⊢ Δ, ℕ }} by mauto 3.
  assert {{ Δ, ℕ ⊢s q σ : Γ, ℕ }} by mauto 3.
  assert {{ ⊢ Δ, ℕ, A[q σ] }} by mauto 3.
  assert {{ Δ ⊢s Id : Δ }} by mauto 2.
  assert {{ Δ ⊢s σ,,M ≈ σ,,zero : Γ, ℕ }} as -> by mauto 3.
  assert {{ Δ, ℕ ⊢s Wk : Δ }} by mauto 2.
  assert {{ Δ, ℕ, A[q σ] ⊢s Wk : Δ, ℕ }} by mauto 2.
  assert {{ Δ ⊢ zero : ℕ }} by mauto 3.
  assert {{ Δ ⊢ zero[σ] ≈ zero : ℕ }} by mauto 3.
  assert {{ Δ ⊢ A[q σ][Id,,zero] ≈ A[σ,,zero] : Type@i }} by mauto 3.
  assert {{ Δ ⊢ A[σ,,zero] ≈ A[σ,,zero[σ]] : Type@i }} by (symmetry; mauto 4).
  assert {{ Γ ⊢ zero : ℕ }} by mauto 3.
  assert {{ Δ ⊢ A[σ,,zero[σ]] ≈ A[Id,,zero][σ] : Type@i }} by mauto 3.
  assert {{ Δ ⊢ A[q σ][Id,,zero] ≈ A[σ,,zero] : Type@i }} as <- by mauto 2.
  assert {{ Δ ⊢ MZ[σ] : A[q σ][Id,,zero] }} by bulky_rewrite.
  assert {{ Δ, ℕ, A[q σ] ⊢s Wk∘Wk,,succ #1 : Δ, ℕ }} by mauto 4.
  assert {{ Δ, ℕ, A[q σ] ⊢ MS[q (q σ)] : A[q σ][Wk∘Wk,,succ #1] }} by (rewrite @exp_eq_typ_q_sigma_then_weak_weak_extend_succ_var_1; mauto 3).
  pose (R := {{{ rec zero return A[q σ] | zero -> MZ[σ] | succ -> MS[q (q σ)] end }}}).
  assert
    {{ Δ ⊢ R ≈ rec M return A[q σ] | zero -> MZ[σ] | succ -> MS[q (q σ)] end : A[q σ][Id,,zero] }} as <-
      by (econstructor; try eapply exp_eq_refl; mauto 3).
  assert
    {{ Δ ⊢ R ≈ MZ[σ] : A[q σ][Id,,zero] }} as ->
      by (econstructor; mauto 3).
  bulky_rewrite.
Qed.

Lemma cons_glu_sub_pred_nat_helper : forall {Γ SbΓ Δ σ ρ i M m},
    {{ EG Γ ∈ glu_ctx_env ↘ SbΓ }} ->
    {{ Δ ⊢s σ ® ρ ∈ SbΓ }} ->
    glu_nat Δ M m ->
    {{ Δ ⊢s σ,,M ® ρ ↦ m ∈ cons_glu_sub_pred i Γ {{{ ℕ }}} SbΓ }}.
Proof.
  intros * ? HM ?.
  assert {{ DG ℕ ∈ glu_univ_elem i ↘ nat_glu_typ_pred i ↘ nat_glu_exp_pred i }} by (glu_univ_elem_econstructor; reflexivity).
  eapply cons_glu_sub_pred_helper; mauto 3.
  econstructor; [unfold nat_glu_typ_pred |]; mauto 3.
Qed.

#[local]
Hint Resolve cons_glu_sub_pred_nat_helper : mcltt.

Lemma glu_rel_exp_natrec_succ_helper : forall {i Γ SbΓ A MZ MS Δ M M' m' σ ρ am P El},
    {{ EG Γ ∈ glu_ctx_env ↘ SbΓ }} ->
    {{ Γ, ℕ ⊩ A : Type@i }} ->
    {{ Γ ⊢ MZ : A[Id,,zero] }} ->
    {{ Γ, ℕ, A ⊩ A[Wk∘Wk,,succ #1] : Type@i }} ->
    {{ Γ, ℕ, A ⊩ MS : A[Wk∘Wk,,succ #1] }} ->
    {{ Δ ⊢ M ≈ succ M' : ℕ }} ->
    glu_nat Δ M' m' ->
    (forall σ ρ am P El,
        {{ Δ ⊢s σ ® ρ ∈ SbΓ }} ->
        {{ ⟦ A ⟧ ρ ↦ m' ↘ am }} ->
        {{ DG am ∈ glu_univ_elem i ↘ P ↘ El }} ->
        exists r,
          {{ rec m' ⟦return A | zero -> MZ | succ -> MS end⟧ ρ ↘ r }} /\
            {{ Δ ⊢ rec M' return A[q σ] | zero -> MZ[σ] | succ -> MS[q (q σ)] end : A[σ,,M'] ® r ∈ El }}) ->
    {{ Δ ⊢s σ ® ρ ∈ SbΓ }} ->
    {{ ⟦ A ⟧ ρ ↦ succ m' ↘ am }} ->
    {{ DG am ∈ glu_univ_elem i ↘ P ↘ El }} ->
    exists r,
      {{ rec succ m' ⟦return A | zero -> MZ | succ -> MS end⟧ ρ ↘ r }} /\
        {{ Δ ⊢ rec M return A[q σ] | zero -> MZ[σ] | succ -> MS[q (q σ)] end : A[σ,,M] ® r ∈ El }}.
Proof.
  intros * ? HA ? ? HMS **.
  assert {{ ⊩ Γ }} by (eexists; eassumption).
  assert {{ Γ ⊩ ℕ : Type@i }} as Hℕ by mauto 3.
  pose (SbΓℕ := cons_glu_sub_pred i Γ {{{ ℕ }}} SbΓ).
  assert {{ EG Γ, ℕ ∈ glu_ctx_env ↘ SbΓℕ }} by (invert_glu_rel_exp Hℕ; econstructor; mauto 3; reflexivity).
  assert {{ Γ, ℕ ⊢ A : Type@i }} by mauto 2.
  invert_glu_rel_exp HA.
  pose (SbΓℕA := cons_glu_sub_pred i {{{ Γ, ℕ }}} A SbΓℕ).
  assert {{ EG Γ, ℕ, A ∈ glu_ctx_env ↘ SbΓℕA }} by (econstructor; mauto 3; reflexivity).
  assert {{ Γ, ℕ, A ⊢ MS : A[Wk∘Wk,,succ #1] }} by mauto 2.
  invert_glu_rel_exp HMS.
  assert {{ Δ ⊢s σ,,M' ® ρ ↦ m' ∈ SbΓℕ }} by (unfold SbΓℕ; mauto 3).
  destruct_glu_rel_exp_with_sub.
  simplify_evals.
  match_by_head glu_univ_elem ltac:(fun H => directed invert_glu_univ_elem H).
  apply_predicate_equivalence.
  unfold univ_glu_exp_pred' in *.
  destruct_conjs.
  match goal with
  | _: {{ ⟦ A ⟧ ρ ↦ m' ↘ ~?m }}, _: {{ DG ~?m ∈ glu_univ_elem i ↘ ?P ↘ ?El }} |- _ =>
      rename m into am';
      rename P into P';
      rename El into El'
  end.
  assert {{ ⊢ Δ }} by mauto 2.
  assert {{ ⊢ Δ, ℕ }} by mauto 3.
  assert {{ Δ ⊢s σ : Γ }} by mauto 3.
  assert {{ Δ, ℕ ⊢ A[q σ] : Type@i }} by mauto 3.
  assert {{ ⊢ Δ, ℕ, A[q σ] }} by mauto 2.
  assert {{ Δ ⊢ M' : ℕ }} by mauto 3.
  assert {{ Δ ⊢ ℕ : Type@0 }} by mauto 3.
  assert {{ Δ ⊢ ℕ[σ] ≈ ℕ : Type@0 }} by mauto 3.
  assert {{ Δ ⊢ M' : ℕ[σ] }} by mauto 3.
  assert {{ Δ ⊢ zero : ℕ }} by mauto 3.
  assert {{ Δ ⊢ zero : ℕ[σ] }} by mauto 3.
  assert {{ Δ ⊢ zero[σ] ≈ zero : ℕ }} by mauto 3.
  assert {{ Δ, ℕ ⊢s q σ : Γ, ℕ }} by mauto 3.
  assert {{ Δ ⊢ A[q σ][Id,,zero] ≈ A[σ,,zero] : Type@i }} by mauto 3.
  assert {{ Δ ⊢ A[σ,,zero] ≈ A[σ,,zero[σ]] : Type@i }} by (symmetry; mauto 4).
  assert {{ Γ ⊢ zero : ℕ }} by mauto 3.
  assert {{ Δ ⊢ A[σ,,zero[σ]] ≈ A[Id,,zero][σ] : Type@i }} by mauto 4.
  assert {{ Δ ⊢ MZ[σ] : A[q σ][Id,,zero] }} by bulky_rewrite.
  assert {{ Δ, ℕ, A[q σ] ⊢s Wk∘Wk,,succ #1 : Δ, ℕ }} by mauto 3.
  assert {{ Δ, ℕ, A[q σ] ⊢ MS[q (q σ)] : A[q σ][Wk∘Wk,,succ #1] }} by (rewrite @exp_eq_typ_q_sigma_then_weak_weak_extend_succ_var_1; mauto 3).
  pose (R := {{{ rec M' return A[q σ] | zero -> MZ[σ] | succ -> MS[q (q σ)] end }}}).
  assert (exists r, {{ rec m' ⟦return A | zero -> MZ | succ -> MS end⟧ ρ ↘ r }} /\ {{ Δ ⊢ R : A[σ,,M'] ® r ∈ El' }}) as [r' []] by mauto 3.
  assert {{ Δ ⊢ R : A[σ,,M'] }} by (erewrite <- @exp_eq_elim_sub_rhs_typ; mauto 3).
  assert {{ Δ ⊢s σ,,M',,R ® ρ ↦ m' ↦ r' ∈ SbΓℕA }} by (unfold SbΓℕA; mauto 3).
  destruct_glu_rel_exp_with_sub.
  simplify_evals.
  match_by_head glu_univ_elem ltac:(fun H => directed invert_glu_univ_elem H).
  apply_predicate_equivalence.
  clear_dups.
  unfold univ_glu_exp_pred' in *.
  destruct_conjs.
  handle_functional_glu_univ_elem.
  match goal with
  | _: {{ ⟦ MS ⟧ ρ ↦ m' ↦ r' ↘ ~?m }} |- _ =>
      rename m into ms
  end.
  exists ms; split; mauto 3.
  assert {{ Δ ⊢s σ,,M ≈ σ,,succ M' : Γ, ℕ }} as -> by mauto 3.
  assert {{ Δ ⊢ succ M' : ℕ }} by mauto 3.
  assert {{ Δ ⊢ succ M' : ℕ[σ] }} by mauto 3.
  assert {{ Δ ⊢ A[σ,,succ M'] ≈ A[q σ][Id,,succ M'] : Type@i }} as -> by mauto 3.
  assert {{ Δ ⊢ rec succ M' return A[q σ] | zero -> MZ[σ] | succ -> MS[q (q σ)] end ≈ rec M return A[q σ] | zero -> MZ[σ] | succ -> MS[q (q σ)] end : A[q σ][Id,,succ M'] }} as <- by (econstructor; mauto 3).
  assert {{ Δ ⊢ rec succ M' return A[q σ] | zero -> MZ[σ] | succ -> MS[q (q σ)] end ≈ MS[q (q σ)][Id,,M',,R] : A[q σ][Id,,succ M'] }} as -> by mauto 2.
  assert {{ Δ ⊢ R : A[q σ][Id,,M'] }} by bulky_rewrite.
  assert {{ Δ ⊢s Id,,M',,R : Δ, ℕ, A[q σ] }} by mauto 3.
  assert {{ Δ ⊢ A[σ,,succ M'] ≈ A[q σ][Id,,succ M'] : Type@i }} as <- by mauto 3.
  assert {{ Δ ⊢ A[Wk∘Wk,,succ #1][σ,,M',,R] ≈ A[σ,,succ M'] : Type@i }} as <- by mauto 3.
  assert {{ Δ ⊢ MS[q (q σ)][Id,,M',,R] ≈ MS[σ,,M',,R] : A[Wk∘Wk,,succ #1][σ,,M',,R] }} as -> by mauto 4.
  eassumption.
Qed.

Lemma cons_glu_sub_pred_q_helper : forall {Γ SbΓ Δ σ ρ i A a},
    {{ EG Γ ∈ glu_ctx_env ↘ SbΓ }} ->
    {{ Δ ⊢s σ ® ρ ∈ SbΓ }} ->
    {{ Γ ⊩ A : Type@i }} ->
    {{ ⟦ A ⟧ ρ ↘ a }} ->
    {{ Δ, A[σ] ⊢s q σ ® ρ ↦ ⇑! a (length Δ) ∈ cons_glu_sub_pred i Γ A SbΓ }}.
Proof.
  intros * ? ? HA ?.
  assert {{ Γ ⊢ A : Type@i }} by mauto 2.
  invert_glu_rel_exp HA.
  destruct_glu_rel_exp_with_sub.
  simplify_evals.
  match_by_head glu_univ_elem ltac:(fun H => directed invert_glu_univ_elem H).
  apply_predicate_equivalence.
  unfold univ_glu_exp_pred' in *.
  destruct_conjs.
  assert {{ Δ ⊢s σ : Γ }} by mauto 2.
  assert {{ ⊢ Δ, A[σ] }} by mauto 3.
  assert {{ Δ, A[σ] ⊢w Wk : Δ }} by mauto 2.
  eapply cons_glu_sub_pred_helper; mauto 2.
  - eapply glu_ctx_env_sub_monotone; eassumption.
  - assert {{ Δ, A[σ] ⊢s Wk : Δ }} by mauto 2.
    assert {{ Δ, A[σ] ⊢ A[σ∘Wk] ≈ A[σ][Wk] : Type@i }} as -> by mauto 3.
    eapply var0_glu_elem; eassumption.
Qed.

#[local]
Hint Resolve cons_glu_sub_pred_q_helper : mcltt.

Lemma cons_glu_sub_pred_q_nat_helper : forall {Γ SbΓ Δ σ ρ i},
    {{ EG Γ ∈ glu_ctx_env ↘ SbΓ }} ->
    {{ Δ ⊢s σ ® ρ ∈ SbΓ }} ->
    {{ Δ, ℕ ⊢s q σ ® ρ ↦ ⇑! ℕ (length Δ) ∈ cons_glu_sub_pred i Γ {{{ ℕ }}} SbΓ }}.
Proof.
  intros.
  assert {{ ⊩ Γ }} by (eexists; eassumption).
  assert {{ Γ ⊩ ℕ : Type@i }} as Hℕ by mauto 3.
  assert {{ ⟦ ℕ ⟧ ρ ↘ ℕ }} by mauto 3.
  assert {{ Δ, ℕ[σ] ⊢s q σ ® ρ ↦ ⇑! ℕ (length Δ) ∈ cons_glu_sub_pred i Γ {{{ ℕ }}} SbΓ }} by mauto 3.
  assert {{ Δ ⊢ ℕ[σ] ≈ ℕ : Type@i }} by mauto 4.
  assert {{ EG Γ, ℕ ∈ glu_ctx_env ↘ cons_glu_sub_pred i Γ {{{ ℕ }}} SbΓ }}
    by (invert_glu_rel_exp Hℕ; econstructor; mauto 3; reflexivity).
  assert {{ ⊢ Δ }} by mauto 2.
  cbn.
  assert {{ ⊢ Δ, ℕ[σ] ≈ Δ, ℕ }} as <- by mauto 3.
  eassumption.
Qed.

#[local]
Hint Resolve cons_glu_sub_pred_q_nat_helper : mcltt.

Lemma glu_rel_exp_natrec_neut_helper : forall {i Γ SbΓ A MZ MS Δ M m σ ρ am P El},
    {{ EG Γ ∈ glu_ctx_env ↘ SbΓ }} ->
    {{ Γ, ℕ ⊩ A : Type@i }} ->
    {{ Γ ⊩ A[Id,,zero] : Type@i }} ->
    {{ Γ ⊩ MZ : A[Id,,zero] }} ->
    {{ Γ, ℕ, A ⊩ A[Wk∘Wk,,succ #1] : Type@i }} ->
    {{ Γ, ℕ, A ⊩ MS : A[Wk∘Wk,,succ #1] }} ->
    {{ Dom m ≈ m ∈ per_bot }} ->
    (forall Δ' τ V, {{ Δ' ⊢w τ : Δ }} -> {{ Rne m in length Δ' ↘ V }} -> {{ Δ' ⊢ M[τ] ≈ V : ℕ }}) ->
    {{ Δ ⊢s σ ® ρ ∈ SbΓ }} ->
    {{ ⟦ A ⟧ ρ ↦ ⇑ ℕ m ↘ am }} ->
    {{ DG am ∈ glu_univ_elem i ↘ P ↘ El }} ->
    exists r,
      {{ rec ⇑ ℕ m ⟦return A | zero -> MZ | succ -> MS end⟧ ρ ↘ r }} /\
        {{ Δ ⊢ rec M return A[q σ] | zero -> MZ[σ] | succ -> MS[q (q σ)] end : A[σ,,M] ® r ∈ El }}.
Proof.
  intros * ? HA ? HMZ ? HMS **.
  assert {{ Γ ⊢ MZ : A[Id,,zero] }} by mauto 2.
  invert_glu_rel_exp HMZ.
  assert {{ ⊩ Γ }} by (eexists; eassumption).
  assert {{ Γ ⊩ ℕ : Type@i }} as Hℕ by mauto 3.
  pose (SbΓℕ := cons_glu_sub_pred i Γ {{{ ℕ }}} SbΓ).
  assert {{ EG Γ, ℕ ∈ glu_ctx_env ↘ SbΓℕ }} by (invert_glu_rel_exp Hℕ; econstructor; mauto 3; reflexivity).
  assert {{ Γ, ℕ ⊢ A : Type@i }} by mauto 2.
  pose proof HA.
  invert_glu_rel_exp HA.
  pose (SbΓℕA := cons_glu_sub_pred i {{{ Γ, ℕ }}} A SbΓℕ).
  assert {{ EG Γ, ℕ, A ∈ glu_ctx_env ↘ SbΓℕA }} by (econstructor; mauto 3; reflexivity).
  assert {{ Δ ⊢s σ,,M ® ρ ↦ ⇑ ℕ m ∈ SbΓℕ }} by (unfold SbΓℕ; mauto 3).
  assert {{ Γ, ℕ, A ⊢ MS : A[Wk∘Wk,,succ #1] }} by mauto 2.
  invert_glu_rel_exp HMS.
  destruct_glu_rel_exp_with_sub.
  simplify_evals.
  match_by_head glu_univ_elem ltac:(fun H => directed invert_glu_univ_elem H).
  apply_predicate_equivalence.
  unfold univ_glu_exp_pred' in *.
  destruct_conjs.
  handle_functional_glu_univ_elem.
  match goal with
  | _: {{ ⟦ MZ ⟧ ~?ρ0 ↘ ~?m }}, _: {{ ⟦ A ⟧ ~?ρ0 ↦ zero ↘ ~?a }} |- _ =>
      rename ρ0 into ρ;
      rename m into mz;
      rename a into az
  end.
  eexists; split; mauto 3.
  assert {{ Δ ⊢s σ : Γ }} by mauto 3.
  assert {{ ⊢ Δ }} by mauto 2.
  assert {{ ⊢ Δ, ℕ }} by mauto 3.
  assert {{ Δ, ℕ ⊢ A[q σ] : Type@i }} by mauto 3.
  assert {{ ⊢ Δ, ℕ, A[q σ] }} by mauto 2.
  assert {{ Δ ⊢ M : ℕ }} by mauto 3.
  assert {{ Δ ⊢ ℕ : Type@0 }} by mauto 3.
  assert {{ Δ ⊢ ℕ[σ] ≈ ℕ : Type@0 }} by mauto 3.
  assert {{ Δ ⊢ M : ℕ[σ] }} by mauto 3.
  assert {{ Δ ⊢ zero : ℕ }} by mauto 3.
  assert {{ Δ ⊢ zero[σ] ≈ zero : ℕ }} by mauto 3.
  assert {{ Δ, ℕ ⊢s q σ : Γ, ℕ }} by mauto 3.
  assert {{ Δ ⊢ A[q σ][Id,,zero] ≈ A[σ,,zero] : Type@i }} by mauto 3.
  assert {{ Δ ⊢ A[σ,,zero] ≈ A[σ,,zero[σ]] : Type@i }} by (symmetry; mauto 4).
  assert {{ Γ ⊢ zero : ℕ }} by mauto 3.
  assert {{ Δ ⊢ A[σ,,zero[σ]] ≈ A[Id,,zero][σ] : Type@i }} by mauto 4.
  assert {{ Δ ⊢ MZ[σ] : A[q σ][Id,,zero] }} by bulky_rewrite.
  assert {{ Δ, ℕ, A[q σ] ⊢s Wk∘Wk,,succ #1 : Δ, ℕ }} by mauto 3.
  assert {{ Δ, ℕ, A[q σ] ⊢ MS[q (q σ)] : A[q σ][Wk∘Wk,,succ #1] }} by (rewrite @exp_eq_typ_q_sigma_then_weak_weak_extend_succ_var_1; mauto 3).
  pose (R := {{{ rec M return A[q σ] | zero -> MZ[σ] | succ -> MS[q (q σ)] end }}}).
  enough {{ Δ ⊢ R : A[σ,,M] ® rec m under ρ return A | zero -> mz | succ -> MS end ∈ glu_elem_bot i am }} by (eapply realize_glu_elem_bot; mauto 3).
  econstructor; mauto 3.
  - erewrite <- @exp_eq_elim_sub_rhs_typ; mauto 3.
  - assert {{ Δ ⊢ MZ[σ] : A[Id,,zero][σ] ® mz ∈ glu_elem_top i az }} as [] by (eapply realize_glu_elem_top; eassumption).
    handle_functional_glu_univ_elem.
    assert {{ ⊨ Γ }} as [env_relΓ] by mauto 3 using completeness_fundamental_ctx.
    assert {{ Γ, ℕ ⊨ A : Type@i }} as [env_relΓℕ] by mauto 3 using completeness_fundamental_exp.
    assert {{ Γ, ℕ, A ⊨ MS : A[Wk∘Wk,,succ #1] }} as [env_relΓℕA] by mauto 3 using completeness_fundamental_exp.
    destruct_conjs.
    pose env_relΓℕA.
    match_by_head (per_ctx_env env_relΓℕA) ltac:(fun H => invert_per_ctx_env H).
    match_by_head (per_ctx_env env_relΓℕ) ltac:(fun H => invert_per_ctx_env H).
    intros s.
    enough (exists r, {{ Rne rec m under ρ return A | zero -> mz | succ -> MS end in s ↘ r }}) as [] by (eexists; split; eassumption).
    assert {{ Dom ρ ≈ ρ ∈ env_relΓ }} by (eapply glu_ctx_env_per_env; revgoals; eassumption).
    destruct_rel_typ.
    invert_rel_typ_body.
    assert {{ Dom ! s ≈ ! s ∈ per_bot }} by mauto 3.
    assert {{ Dom ρ ↦ ⇑! ℕ s ≈ ρ ↦ ⇑! ℕ s ∈ env_relΓℕ }} by (apply_relation_equivalence; unshelve eexists; simpl; intuition).
    assert {{ Dom ρ ↦ succ ⇑! ℕ s ≈ ρ ↦ succ ⇑! ℕ s ∈ env_relΓℕ }} by (apply_relation_equivalence; unshelve eexists; simpl; intuition).
    destruct_rel_typ.
    invert_rel_typ_body.
    match goal with
    | _: {{ ⟦ A ⟧ ρ ↦ ⇑! ℕ s ↘ ~?a }}, _: {{ ⟦ A ⟧ ρ ↦ (succ ⇑! ℕ s) ↘ ~?a' }} |- _ =>
        rename a into as';