From a367591e9a67e5cc33cfd6e4d85a9d932fa74f6a Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Thu, 17 Apr 2025 15:15:58 -0400 Subject: [PATCH] Add extensional version of pair equality rules --- theories/logrel.v | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/theories/logrel.v b/theories/logrel.v index f85b32e..fa50b9c 100644 --- a/theories/logrel.v +++ b/theories/logrel.v @@ -1521,6 +1521,22 @@ Proof. rewrite /DJoin.R. hauto lq:on ctrs:rtc,RERed.R. Qed. +Lemma SE_PairExt Γ (a b : PTm) A B i : + Γ ⊨ PBind PSig A B ∈ PUniv i -> + Γ ⊨ a ∈ PBind PSig A B -> + Γ ⊨ b ∈ PBind PSig A B -> + Γ ⊨ PProj PL a ≡ PProj PL b ∈ A -> + Γ ⊨ PProj PR a ≡ PProj PR b ∈ subst_PTm (scons (PProj PL a) VarPTm) B -> + Γ ⊨ a ≡ b ∈ PBind PSig A B. +Proof. + move => h0 ha hb h1 h2. + suff h : Γ ⊨ a ≡ PPair (PProj PL a) (PProj PR a) ∈ PBind PSig A B /\ + Γ ⊨ PPair (PProj PL b) (PProj PR b) ≡ b ∈ PBind PSig A B /\ + Γ ⊨ PPair (PProj PL a) (PProj PR a) ≡ PPair (PProj PL b) (PProj PR b) ∈ PBind PSig A B + by decompose [and] h; eauto using SE_Transitive, SE_Symmetric. + eauto 20 using SE_PairEta, SE_Symmetric, SE_Pair. +Qed. + Lemma SE_FunExt Γ (a b : PTm) A B i : Γ ⊨ PBind PPi A B ∈ PUniv i -> Γ ⊨ a ∈ PBind PPi A B ->