From ebbadc6667ba36d7999e5d7cf4bebb8811ce7c39 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Thu, 7 Nov 2024 22:51:21 -0800
Subject: [PATCH] update lemmas

---
 .../Soundness/LogicalRelation/CoreLemmas.v    | 26 ++++++++++++++++++-
 1 file changed, 25 insertions(+), 1 deletion(-)

diff --git a/theories/Core/Soundness/LogicalRelation/CoreLemmas.v b/theories/Core/Soundness/LogicalRelation/CoreLemmas.v
index 625654e..08ea53e 100644
--- a/theories/Core/Soundness/LogicalRelation/CoreLemmas.v
+++ b/theories/Core/Soundness/LogicalRelation/CoreLemmas.v
@@ -686,7 +686,7 @@ Qed.
             end);
   eauto; intuition.
 
-Lemma glu_univ_elem_resp_per_univ : forall i a a' R,
+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 }} ->
@@ -798,6 +798,30 @@ Proof.
     mauto.
 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.
+
+
 (** *** Morphism instances for [glu_univ_elem] *)
 Add Parametric Morphism i : (glu_univ_elem i)
     with signature glu_typ_pred_equivalence ==> glu_exp_pred_equivalence ==> per_univ i ==> iff as glu_univ_elem_morphism_iff.