From 907d468c23e2e0a77a0450eaeaec8262c4241277 Mon Sep 17 00:00:00 2001 From: HuStmpHrrr Date: Sat, 4 May 2024 12:31:14 -0400 Subject: [PATCH] shorter --- theories/Core/Semantic/PERLemmas.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/theories/Core/Semantic/PERLemmas.v b/theories/Core/Semantic/PERLemmas.v index b04873ab..c832b5b5 100644 --- a/theories/Core/Semantic/PERLemmas.v +++ b/theories/Core/Semantic/PERLemmas.v @@ -260,7 +260,7 @@ Proof with solve [mauto]. specialize (H1 _ _ equiv_c_c) as [? ? ? ? [? ?]]. specialize (H9 _ _ equiv_c_c') as []. per_univ_elem_irrel_rewrite. - econstructor; eauto. firstorder. + firstorder (econstructor; eauto). + setoid_rewrite H2. intros. assert (equiv_c'_c' : in_rel c' c') by (etransitivity; [symmetry | ]; eassumption). @@ -270,8 +270,7 @@ Proof with solve [mauto]. specialize (H3 _ _ equiv_c_c') as []. specialize (H4 _ _ equiv_c'_c') as []. per_univ_elem_irrel_rewrite. - econstructor; eauto. - firstorder. + firstorder (econstructor; eauto). - split; try per_univ_elem_econstructor... Qed.