From 5e01c6531322c6a6d26d13916d193aaabb014a13 Mon Sep 17 00:00:00 2001 From: "Junyoung/\"Clare\" Jang" Date: Tue, 13 Aug 2024 17:49:52 -0400 Subject: [PATCH] Update files --- .../Soundness/LogicalRelation/CoreLemmas.v | 82 ++++++- .../Core/Soundness/LogicalRelation/Lemmas.v | 205 +++++++++++++++--- theories/Core/Soundness/Realizability.v | 10 + 3 files changed, 268 insertions(+), 29 deletions(-) diff --git a/theories/Core/Soundness/LogicalRelation/CoreLemmas.v b/theories/Core/Soundness/LogicalRelation/CoreLemmas.v index 336f4b80..d57d9b1a 100644 --- a/theories/Core/Soundness/LogicalRelation/CoreLemmas.v +++ b/theories/Core/Soundness/LogicalRelation/CoreLemmas.v @@ -786,7 +786,6 @@ Proof. mauto 3. Qed. - Lemma glu_univ_elem_exp_monotone : forall i a P El, {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} -> forall Δ σ Γ M A m, @@ -850,10 +849,89 @@ Proof. * mauto 3. Qed. +Add Parametric Morphism i a : (glu_elem_bot i a) + with signature wf_ctx_eq ==> eq ==> eq ==> eq ==> iff as glu_elem_bot_morphism_iff1. +Proof. + intros Γ Γ' HΓΓ' *. + split; intros []; econstructor; mauto 4; [rewrite <- HΓΓ' | rewrite -> HΓΓ']; eassumption. +Qed. + +Add Parametric Morphism i a Γ : (glu_elem_bot i a Γ) + with signature wf_exp_eq Γ {{{ Type@i }}} ==> eq ==> eq ==> iff as glu_elem_bot_morphism_iff2. +Proof. + intros A A' HAA' *. + split; intros []; econstructor; mauto 3; [rewrite <- HAA' | | rewrite -> HAA' |]; + try eassumption; + intros; + assert {{ Δ ⊢ A[σ] ≈ A'[σ] : Type@i }} as HAσA'σ by mauto 4; + [rewrite <- HAσA'σ | rewrite -> HAσA'σ]; + mauto. +Qed. + +Add Parametric Morphism i a Γ A : (glu_elem_bot i a Γ A) + with signature wf_exp_eq Γ A ==> eq ==> iff as glu_elem_bot_morphism_iff3. +Proof. + intros M M' HMM' *. + split; intros []; econstructor; mauto 3; try (gen_presup HMM'; eassumption); + intros; + assert {{ Δ ⊢ M[σ] ≈ M'[σ] : A[σ] }} as HMσM'σ by mauto 4; + [rewrite <- HMσM'σ | rewrite -> HMσM'σ]; + mauto. +Qed. + +Add Parametric Morphism i a : (glu_elem_top i a) + with signature wf_ctx_eq ==> eq ==> eq ==> eq ==> iff as glu_elem_top_morphism_iff1. +Proof. + intros Γ Γ' HΓΓ' *. + split; intros []; econstructor; mauto 4; [rewrite <- HΓΓ' | rewrite -> HΓΓ']; eassumption. +Qed. + +Add Parametric Morphism i a Γ : (glu_elem_top i a Γ) + with signature wf_exp_eq Γ {{{ Type@i }}} ==> eq ==> eq ==> iff as glu_elem_top_morphism_iff2. +Proof. + intros A A' HAA' *. + split; intros []; econstructor; mauto 3; [rewrite <- HAA' | | rewrite -> HAA' |]; + try eassumption; + intros; + assert {{ Δ ⊢ A[σ] ≈ A'[σ] : Type@i }} as HAσA'σ by mauto 4; + [rewrite <- HAσA'σ | rewrite -> HAσA'σ]; + mauto. +Qed. + +Add Parametric Morphism i a Γ A : (glu_elem_top i a Γ A) + with signature wf_exp_eq Γ A ==> eq ==> iff as glu_elem_top_morphism_iff3. +Proof. + intros M M' HMM' *. + split; intros []; econstructor; mauto 3; try (gen_presup HMM'; eassumption); + intros; + assert {{ Δ ⊢ M[σ] ≈ M'[σ] : A[σ] }} as HMσM'σ by mauto 4; + [rewrite <- HMσM'σ | rewrite -> HMσM'σ]; + mauto. +Qed. + +Add Parametric Morphism i a : (glu_typ_top i a) + with signature wf_ctx_eq ==> eq ==> iff as glu_typ_top_morphism_iff1. +Proof. + intros Γ Γ' HΓΓ' *. + split; intros []; econstructor; mauto 4. +Qed. + +Add Parametric Morphism i a Γ : (glu_typ_top i a Γ) + with signature wf_exp_eq Γ {{{ Type@i }}} ==> iff as glu_typ_top_morphism_iff2. +Proof. + intros A A' HAA' *. + split; intros []; econstructor; mauto 3; + try (gen_presup HAA'; eassumption); + intros; + assert {{ Δ ⊢ A[σ] ≈ A'[σ] : Type@i }} as HAσA'σ by mauto 4; + [rewrite <- HAσA'σ | rewrite -> HAσA'σ]; + mauto. +Qed. + (* Simple Morphism instance for "glu_ctx_env" *) Add Parametric Morphism : glu_ctx_env with signature glu_sub_pred_equivalence ==> eq ==> iff as simple_glu_ctx_env_morphism_iff. -Proof with mautosolve. +Proof. intros Sb Sb' HSbSb' a. split; intro Horig; [gen Sb' | gen Sb]; induction Horig; econstructor; diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v index f72a5791..74410c3a 100644 --- a/theories/Core/Soundness/LogicalRelation/Lemmas.v +++ b/theories/Core/Soundness/LogicalRelation/Lemmas.v @@ -9,6 +9,31 @@ From Mcltt.Core.Soundness Require Import LogicalRelation.Core. From Mcltt.Core.Syntactic Require Import Corollaries. Import Domain_Notations. +Add Parametric Morphism i a Γ A M : (glu_elem_bot i a Γ A M) + with signature per_bot ==> iff as glu_elem_bot_morphism_iff4. +Proof. + intros m m' Hmm' *. + split; intros []; econstructor; mauto 3; + try (etransitivity; mauto 4); + intros; + specialize (Hmm' (length Δ)) as [? []]; + functional_read_rewrite_clear; + mauto. +Qed. + +Add Parametric Morphism i a Γ A M R (H : per_univ_elem i R a a) : (glu_elem_top i a Γ A M) + with signature R ==> iff as glu_elem_top_morphism_iff4. +Proof. + intros m m' Hmm' *. + split; intros []; econstructor; mauto 3; + pose proof (per_elem_then_per_top H Hmm') as Hmm''; + try (etransitivity; mauto 4); + intros; + specialize (Hmm'' (length Δ)) as [? []]; + functional_read_rewrite_clear; + mauto. +Qed. + Lemma glu_univ_elem_typ_escape : forall {i j a P P' El El' Γ A A'}, {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} -> {{ DG a ∈ glu_univ_elem j ↘ P' ↘ El' }} -> @@ -231,7 +256,7 @@ Section glu_univ_elem_cumulativity. Qed. End glu_univ_elem_cumulativity. -Corollary glu_univ_elem_typ_cumu_ge : forall {i j a P P' El El' Γ A}, +Corollary glu_univ_elem_typ_cumu_ge : forall {i j a P P' El El' Γ A}, i <= j -> {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} -> {{ DG a ∈ glu_univ_elem j ↘ P' ↘ El' }} -> @@ -242,17 +267,61 @@ Proof. eapply glu_univ_elem_cumulativity_ge; mauto. Qed. -Corollary glu_univ_elem_exp_cumu_ge : forall {i j a P P' El El' Γ A M m}, +Corollary glu_univ_elem_typ_cumu_max_left : forall {i j a P P' El El' Γ A}, + {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} -> + {{ DG a ∈ glu_univ_elem (max i j) ↘ P' ↘ El' }} -> + {{ Γ ⊢ A ® P }} -> + {{ Γ ⊢ A ® P' }}. +Proof. + intros. + assert (i <= max i j) by lia. + eapply glu_univ_elem_typ_cumu_ge; mauto. +Qed. + +Corollary glu_univ_elem_typ_cumu_max_right : forall {i j a P P' El El' Γ A}, + {{ DG a ∈ glu_univ_elem j ↘ P ↘ El }} -> + {{ DG a ∈ glu_univ_elem (max i j) ↘ P' ↘ El' }} -> + {{ Γ ⊢ A ® P }} -> + {{ Γ ⊢ A ® P' }}. +Proof. + intros. + assert (j <= max i j) by lia. + eapply glu_univ_elem_typ_cumu_ge; mauto. +Qed. + +Corollary glu_univ_elem_exp_cumu_ge : forall {i j a P P' El El' Γ A M m}, i <= j -> {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} -> {{ DG a ∈ glu_univ_elem j ↘ P' ↘ El' }} -> {{ Γ ⊢ M : A ® m ∈ El }} -> {{ Γ ⊢ M : A ® m ∈ El' }}. Proof. - intros * ? ? ?. gen m M A Γ. + intros. gen m M A Γ. eapply glu_univ_elem_cumulativity_ge; mauto. Qed. +Corollary glu_univ_elem_exp_cumu_max_left : forall {i j a P P' El El' Γ A M m}, + {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} -> + {{ DG a ∈ glu_univ_elem (max i j) ↘ P' ↘ El' }} -> + {{ Γ ⊢ M : A ® m ∈ El }} -> + {{ Γ ⊢ M : A ® m ∈ El' }}. +Proof. + intros. + assert (i <= max i j) by lia. + eapply glu_univ_elem_exp_cumu_ge; mauto. +Qed. + +Corollary glu_univ_elem_exp_cumu_max_right : forall {i j a P P' El El' Γ A M m}, + {{ DG a ∈ glu_univ_elem j ↘ P ↘ El }} -> + {{ DG a ∈ glu_univ_elem (max i j) ↘ P' ↘ El' }} -> + {{ Γ ⊢ M : A ® m ∈ El }} -> + {{ Γ ⊢ M : A ® m ∈ El' }}. +Proof. + intros. + assert (j <= max i j) by lia. + eapply glu_univ_elem_exp_cumu_ge; mauto. +Qed. + Corollary glu_univ_elem_exp_lower : forall {i j a P P' El El' Γ A M m}, i <= j -> {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} -> @@ -265,6 +334,30 @@ Proof. eapply glu_univ_elem_cumulativity_ge; mauto. Qed. +Corollary glu_univ_elem_exp_lower_max_left : forall {i j a P P' El El' Γ A M m}, + {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} -> + {{ DG a ∈ glu_univ_elem (max i j) ↘ P' ↘ El' }} -> + {{ Γ ⊢ A ® P }} -> + {{ Γ ⊢ M : A ® m ∈ El' }} -> + {{ Γ ⊢ M : A ® m ∈ El }}. +Proof. + intros. + assert (i <= max i j) by lia. + eapply glu_univ_elem_exp_lower; mauto. +Qed. + +Corollary glu_univ_elem_exp_lower_max_right : forall {i j a P P' El El' Γ A M m}, + {{ DG a ∈ glu_univ_elem j ↘ P ↘ El }} -> + {{ DG a ∈ glu_univ_elem (max i j) ↘ P' ↘ El' }} -> + {{ Γ ⊢ A ® P }} -> + {{ Γ ⊢ M : A ® m ∈ El' }} -> + {{ Γ ⊢ M : A ® m ∈ El }}. +Proof. + intros. + assert (j <= max i j) by lia. + eapply glu_univ_elem_exp_lower; mauto. +Qed. + Lemma glu_univ_elem_exp_conv : forall {i j k a a' P P' El El' Γ A M m}, {{ Dom a ≈ a' ∈ per_univ k }} -> {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} -> @@ -274,16 +367,13 @@ Lemma glu_univ_elem_exp_conv : forall {i j k a a' P P' El El' Γ A M m}, {{ Γ ⊢ M : A ® m ∈ El' }}. Proof. intros * [] ? ? ? ?. - assert {{ Dom a ≈ a' ∈ per_univ (max i k) }} by (eexists; mauto using per_univ_elem_cumu_max_right). + assert {{ Dom a ≈ a' ∈ per_univ (max i k) }} as Haa' by (eexists; mauto using per_univ_elem_cumu_max_right). assert (exists P El, {{ DG a ∈ glu_univ_elem (max i k) ↘ P ↘ El }}) as [Pik [Elik]] by mauto using glu_univ_elem_cumu_max_left. - assert {{ DG a' ∈ glu_univ_elem (max i k) ↘ Pik ↘ Elik }} by (erewrite <- glu_univ_elem_morphism_iff; try reflexivity; mauto). - assert (i <= max i k) by lia. - assert {{ Γ ⊢ M : A ® m ∈ Elik }} by (eapply glu_univ_elem_exp_cumu_ge; mauto). + assert {{ DG a' ∈ glu_univ_elem (max i k) ↘ Pik ↘ Elik }} by (setoid_rewrite <- Haa'; eassumption). + assert {{ Γ ⊢ M : A ® m ∈ Elik }} by (eapply glu_univ_elem_exp_cumu_max_left; [| | eassumption]; eassumption). assert (exists P El, {{ DG a' ∈ glu_univ_elem (max j (max i k)) ↘ P ↘ El }}) as [Ptop [Eltop]] by mauto using glu_univ_elem_cumu_max_right. - assert (max i k <= max j (max i k)) by lia. - assert {{ Γ ⊢ M : A ® m ∈ Eltop }} by (eapply glu_univ_elem_exp_cumu_ge; mauto). - assert (j <= max j (max i k)) by lia. - eapply glu_univ_elem_exp_lower; mauto. + assert {{ Γ ⊢ M : A ® m ∈ Eltop }} by (eapply glu_univ_elem_exp_cumu_max_right; [| | eassumption]; eassumption). + eapply glu_univ_elem_exp_lower_max_left; mauto. Qed. Lemma glu_univ_elem_per_subtyp_typ_escape : forall {i a a' P P' El El' Γ A A'}, @@ -349,16 +439,14 @@ Proof. assert {{ DG b' ∈ glu_univ_elem i ↘ OP' d{{{ ⇑! a' (length Γ) }}} equiv_len'_len' ↘ OEl' d{{{ ⇑! a' (length Γ) }}} equiv_len'_len' }} by mauto. assert {{ Γ, IT' ⊢ OT ® OP d{{{ ⇑! a (length Γ) }}} equiv_len_len }}. { - assert {{ Γ, IT ⊢ #0 : IT[Wk] ® !(length Γ) ∈ glu_elem_bot i a }} by eauto using var_glu_elem_bot. - assert {{ Γ, IT ⊢ #0 : IT[Wk] ® ⇑! a (length Γ) ∈ IEl }} by (eapply realize_glu_elem_bot; mauto). + assert {{ Γ, IT ⊢ #0 : IT[Wk] ® ⇑! a (length Γ) ∈ IEl }} by (eapply var0_glu_elem; mauto). assert {{ ⊢ Γ, IT' ≈ Γ, IT }} as -> by mauto. assert {{ Γ, IT ⊢ OT[Wk,,#0] ≈ OT : Type@i }} as <- by (bulky_rewrite1; mauto 3). mauto. } assert {{ Γ, IT' ⊢ OT' ® OP' d{{{ ⇑! a' (length Γ) }}} equiv_len'_len' }}. { - assert {{ Γ, IT' ⊢ #0 : IT'[Wk] ® !(length Γ) ∈ glu_elem_bot i a' }} by eauto using var_glu_elem_bot. - assert {{ Γ, IT' ⊢ #0 : IT'[Wk] ® ⇑! a' (length Γ) ∈ IEl }} by (eapply realize_glu_elem_bot; mauto). + assert {{ Γ, IT' ⊢ #0 : IT'[Wk] ® ⇑! a' (length Γ) ∈ IEl }} by (eapply var0_glu_elem; mauto). assert {{ Γ, IT' ⊢ OT'[Wk,,#0] ® OP' d{{{ ⇑! a' (length Γ) }}} equiv_len'_len' }} by mauto. assert {{ Γ, IT' ⊢ OT'[Wk,,#0] ≈ OT' : Type@i }} as <- by (bulky_rewrite1; mauto 3). mauto. @@ -475,6 +563,60 @@ Proof. eapply glu_univ_elem_exp_lower; mauto. Qed. +Lemma glu_ctx_env_sub_resp_ctx_eq : forall {Γ Sb}, + {{ EG Γ ∈ glu_ctx_env ↘ Sb }} -> + forall {Δ Δ' σ p}, + {{ Δ ⊢s σ ® p ∈ Sb }} -> + {{ ⊢ Δ ≈ Δ' }} -> + {{ Δ' ⊢s σ ® p ∈ Sb }}. +Proof. + induction 1; intros * HSb Hctxeq; + apply_predicate_equivalence; + simpl in *; + mauto. + + destruct_by_head cons_glu_sub_pred. + econstructor; mauto 4. + rewrite <- Hctxeq; eassumption. +Qed. + +Add Parametric Morphism Sb Γ (H : glu_ctx_env Sb Γ) : Sb + with signature wf_ctx_eq ==> eq ==> eq ==> iff as glu_ctx_env_sub_morphism_iff1. +Proof. + intros. + split; intros; eapply glu_ctx_env_sub_resp_ctx_eq; mauto. +Qed. + +Lemma glu_ctx_env_sub_resp_sub_eq : forall {Γ Sb}, + {{ EG Γ ∈ glu_ctx_env ↘ Sb }} -> + forall {Δ σ σ' p}, + {{ Δ ⊢s σ ® p ∈ Sb }} -> + {{ Δ ⊢s σ ≈ σ' : Γ }} -> + {{ Δ ⊢s σ' ® p ∈ Sb }}. +Proof. + induction 1; intros * HSb Hsubeq; + apply_predicate_equivalence; + simpl in *; + gen_presup Hsubeq; + try eassumption. + + destruct_by_head cons_glu_sub_pred. + econstructor; mauto 4. + assert {{ Γ, A ⊢s Wk : Γ }} by mauto 3. + assert {{ Δ ⊢s Wk∘σ ≈ Wk∘σ' : Γ }} by mauto 3. + assert {{ Δ ⊢ A[Wk∘σ] ≈ A[Wk∘σ'] : Type@i }} as <- by mauto 3. + assert {{ Δ ⊢ #0[σ] ≈ #0[σ'] : A[Wk][σ] }} by mauto 3. + assert {{ Δ ⊢ #0[σ] ≈ #0[σ'] : A[Wk∘σ] }} as <- by mauto 3. + eassumption. +Qed. + +Add Parametric Morphism Sb Γ (H : glu_ctx_env Sb Γ) Δ : (Sb Δ) + with signature wf_sub_eq Δ Γ ==> eq ==> iff as glu_ctx_env_sub_morphism_iff2. +Proof. + intros. + split; intros; eapply glu_ctx_env_sub_resp_sub_eq; mauto. +Qed. + Lemma glu_ctx_env_per_env : forall {Γ Sb env_rel Δ σ p}, {{ EG Γ ∈ glu_ctx_env ↘ Sb }} -> {{ EF Γ ≈ Γ ∈ per_ctx_env ↘ env_rel }} -> @@ -496,8 +638,7 @@ Proof. handle_per_univ_elem_irrel. assert (exists P' El', {{ DG a ∈ glu_univ_elem (max i j) ↘ P' ↘ El' }}) as [? []] by mauto using glu_univ_elem_cumu_max_left. eexists; eapply glu_univ_elem_per_elem; mauto using per_univ_elem_cumu_max_right. - assert (i <= max i j) by lia. - eapply glu_univ_elem_exp_cumu_ge; mauto. + eapply glu_univ_elem_exp_cumu_max_left; [| | eassumption]; eassumption. Qed. Lemma glu_ctx_env_wf_ctx : forall {Γ Sb}, @@ -535,7 +676,7 @@ Proof. intros Δ σ p []. saturate_refl_for per_ctx_env. assert {{ Dom ρ ↯ ≈ ρ ↯ ∈ tail_rel }} - by (eapply glu_ctx_env_per_env; only 3: eassumption; eassumption). + by (eapply glu_ctx_env_per_env; [| | eassumption]; eassumption). assert {{ Δ0 ⊢s Wk∘σ0 ® ρ ↯ ∈ TSb' }} by intuition. assert (glu_rel_typ_sub j Δ0 A' {{{ Wk∘σ0 }}} d{{{ ρ ↯ }}}) as [] by mauto. destruct_rel_typ. @@ -617,7 +758,7 @@ Proof. rename a0 into a'. rename P0 into P'. rename El0 into El'. - assert {{ Dom ρ ↯ ≈ ρ ↯ ∈ tail_rel }} by (eapply glu_ctx_env_per_env; only 3: eassumption; eassumption). + assert {{ Dom ρ ↯ ≈ ρ ↯ ∈ tail_rel }} by (eapply glu_ctx_env_per_env; [| | eassumption]; eassumption). assert {{ Sub a <: a' at j }} by mauto 4. assert {{ ⊢ Γ, A ⊆ Γ', A' }} by mauto 3. econstructor; mauto; intuition. @@ -650,9 +791,11 @@ Proof. assert {{ Δ ⊢ A[Wk∘σ0] ≈ A[Wk][σ0] : Type@i }} by mauto 3. assert {{ Δ' ⊢ A[Wk∘σ0][σ] ≈ A[Wk][σ0][σ] : Type@i }} as <- by mauto 3. eassumption. - - assert {{ Δ' ⊢s (Wk ∘ σ0) ∘ σ ® ρ ↯ ∈ TSb }} by mauto. - admit. (* by rewriting *) -Admitted. + - assert {{ Δ' ⊢s σ : Δ }} by mauto 3. + assert {{ Γ, A ⊢s Wk : Γ }} by mauto 3. + assert {{ Δ' ⊢s (Wk ∘ σ0) ∘ σ ≈ Wk ∘ (σ0 ∘ σ) : Γ }} as <- by mauto 3. + mauto. +Qed. Lemma destruct_glu_rel_exp : forall {Γ Sb M A}, {{ EG Γ ∈ glu_ctx_env ↘ Sb }} -> @@ -685,8 +828,16 @@ Proof. functional_eval_rewrite_clear. econstructor; mauto. - eapply realize_glu_elem_bot; mauto. - assert {{ Γ, A[Id] ⊢ #0 : A[Id][Wk] ® !(length Γ) ∈ glu_elem_bot i a }} as [] by (eapply var_glu_elem_bot; mauto). - admit. (* by some rewriting *) - - assert {{ Γ, A ⊢s Id∘Wk ® p ∈ TSb }} by (eapply glu_ctx_env_sub_monotone; mauto 4). - admit. (* by some rewriting *) -Admitted. + assert {{ ⊢ Γ }} by mauto 3. + assert {{ Γ ⊢ A[Id] : Type@i }} by mauto 3. + assert {{ ⊢ Γ, A[Id] ≈ Γ, A }} as <- by mauto 4. + assert {{ Γ, A[Id] ⊢ A[Wk] : Type@i }} by mauto 4. + assert {{ Γ, A[Id] ⊢s Wk : Γ }} by mauto 4. + assert {{ Γ, A[Id] ⊢ A[Id][Wk] ≈ A[Wk∘Id] : Type@i }} as <- by (transitivity {{{ A[Wk] }}}; mauto 4). + assert {{ Γ, A[Id] ⊢ #0 ≈ #0[Id] : A[Id][Wk] }} as <- by mauto. + eapply var_glu_elem_bot; mauto. + - assert {{ Γ, A ⊢s Wk : Γ }} by mauto 4. + assert {{ Γ, A ⊢s Wk∘Id : Γ }} by mauto 4. + assert {{ Γ, A ⊢s Id∘Wk ≈ Wk∘Id : Γ }} as <- by (transitivity {{{ Wk }}}; mauto 3). + eapply glu_ctx_env_sub_monotone; mauto 4. +Qed. diff --git a/theories/Core/Soundness/Realizability.v b/theories/Core/Soundness/Realizability.v index 943b9a9a..c368da0d 100644 --- a/theories/Core/Soundness/Realizability.v +++ b/theories/Core/Soundness/Realizability.v @@ -347,3 +347,13 @@ Qed. #[export] Hint Resolve realize_glu_typ_top realize_glu_elem_top : mcltt. + +Corollary var0_glu_elem : forall {i a P El Γ A}, + {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} -> + {{ Γ ⊢ A ® P }} -> + {{ Γ, A ⊢ #0 : A[Wk] ® ⇑! a (length Γ) ∈ El }}. +Proof. + intros. + eapply realize_glu_elem_bot; mauto 4. + eauto using var_glu_elem_bot. +Qed.