From 9335bd69cdb112d1a2800a2d7c3171aa47f4abe0 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Sat, 4 May 2024 12:24:46 -0400
Subject: [PATCH] simplification

---
 theories/Core/Axioms.v             |  7 -------
 theories/Core/Semantic/PERLemmas.v | 20 ++------------------
 2 files changed, 2 insertions(+), 25 deletions(-)

diff --git a/theories/Core/Axioms.v b/theories/Core/Axioms.v
index d1524798..b92302c3 100644
--- a/theories/Core/Axioms.v
+++ b/theories/Core/Axioms.v
@@ -1,8 +1 @@
 Require Export Coq.Logic.FunctionalExtensionality.
-
-Lemma exists_absorption :
-  forall (A : Type) (P : A -> Prop) (Q : Prop),
-    (exists x : A, P x) /\ Q <-> (exists x : A, P x /\ Q).
-Proof.
-  firstorder.
-Qed.
diff --git a/theories/Core/Semantic/PERLemmas.v b/theories/Core/Semantic/PERLemmas.v
index a91db1b2..b04873ab 100644
--- a/theories/Core/Semantic/PERLemmas.v
+++ b/theories/Core/Semantic/PERLemmas.v
@@ -198,7 +198,7 @@ Proof.
   eauto using per_univ_elem_right_irrel.
 Qed.
 
-Lemma per_univ_elem_cross_irrel1 : forall i A B R B' R',
+Lemma per_univ_elem_cross_irrel : forall i A B R B' R',
     per_univ_elem i A B R ->
     per_univ_elem i B' A R' ->
     R = R'.
@@ -209,17 +209,6 @@ Proof.
   eauto using per_univ_elem_right_irrel.
 Qed.
 
-Lemma per_univ_elem_cross_irrel2 : forall i A B R A' R',
-    per_univ_elem i A B R ->
-    per_univ_elem i B A' R' ->
-    R = R'.
-Proof.
-  intros.
-  apply per_univ_elem_sym in H.
-  destruct_all.
-  eauto using per_univ_elem_right_irrel.
-Qed.
-
 Ltac do_per_univ_elem_irrel_rewrite1 :=
   match goal with
     | H1 : {{ DF ~?A ≈ ~_ ∈ per_univ_elem ?i ↘ ?R1 }},
@@ -235,12 +224,7 @@ Ltac do_per_univ_elem_irrel_rewrite1 :=
     | H1 : {{ DF ~?A ≈ ~_ ∈ per_univ_elem ?i ↘ ?R1 }},
         H2 : {{ DF ~_ ≈ ~?A ∈ per_univ_elem ?i ↘ ?R2 }} |- _ =>
         tryif unify R1 R2 then fail else
-          (let H := fresh "H" in assert (R1 = R2) as H by (eapply per_univ_elem_cross_irrel1; eassumption); subst;
-                                 try rewrite <- H in *)
-    | H1 : {{ DF ~_ ≈ ~?B ∈ per_univ_elem ?i ↘ ?R1 }},
-        H2 : {{ DF ~?B ≈ ~_ ∈ per_univ_elem ?i ↘ ?R2 }} |- _ =>
-        tryif unify R1 R2 then fail else
-          (let H := fresh "H" in assert (R1 = R2) as H by (eapply per_univ_elem_cross_irrel2; eassumption); subst;
+          (let H := fresh "H" in assert (R1 = R2) as H by (eapply per_univ_elem_cross_irrel; eassumption); subst;
                                  try rewrite <- H in *)
     end.