From b166559bc4eb6e653f914c964e8536e3924f7b48 Mon Sep 17 00:00:00 2001
From: melanie-taprogge <melanie.taprogge@icloud.com>
Date: Sun, 6 Sep 2026 16:10:21 +0200
Subject: [PATCH] correct theorem names

---
 PropExt.lp | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/PropExt.lp b/PropExt.lp
index 66a9087..d3f06af 100644
--- a/PropExt.lp
+++ b/PropExt.lp
@@ -262,7 +262,7 @@ end;
 
 // Simplifications on Equalities 
 
-opaque symbol =_idem t (x : τ t) : π ((x = x) = ⊤) ≔
+opaque symbol =_refl t (x : τ t) : π ((x = x) = ⊤) ≔
 begin
   assume t x;
   refine propExt (x = x) ⊤ _ _
@@ -270,7 +270,7 @@ begin
     {assume h1; refine eq_refl x}
 end;
 
-opaque symbol ¬=_idem t (x : τ t) : π (¬ (x = x) = ⊥) ≔
+opaque symbol ¬=_irrefl t (x : τ t) : π (¬ (x = x) = ⊥) ≔
 begin
   assume t x;
   refine propExt (¬ (x = x)) ⊥ _ _
@@ -436,7 +436,7 @@ end;
 
 // Simplifications on Implication
 
-opaque symbol ⇒_idem x : π ((x ⇒ x) = ⊤) ≔
+opaque symbol ⇒_refl x : π ((x ⇒ x) = ⊤) ≔
 begin
   assume x;
   refine propExt (x ⇒ x) ⊤ _ _
@@ -478,7 +478,7 @@ end;
 
 // Simplifications on Bi-Implication
 
-opaque symbol ⇔_idem x : π ((x ⇔ x) = ⊤) ≔
+opaque symbol ⇔_refl x : π ((x ⇔ x) = ⊤) ≔
 begin
   assume x;
   refine propExt (x ⇔ x) ⊤ _ _