From 0b67efc9670c54847a2c4af05d15412a61824db1 Mon Sep 17 00:00:00 2001
From: Ioannis Markakis <70938217+jmarkakis@users.noreply.github.com>
Date: Mon, 2 Oct 2023 10:38:43 +0100
Subject: [PATCH 1/5] Added Irreflexicity and Asymmetry of WellFounded

---
 CHANGELOG.md                   |  8 ++++++++
 src/Induction/WellFounded.agda | 21 ++++++++++++++++++++-
 2 files changed, 28 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3ba0274349..ac84b7f058 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -3514,6 +3514,14 @@ This is a full list of proofs that have changed form to use irrelevant instance
 * Added new proof to `Induction.WellFounded`
   ```agda
   Acc-resp-flip-≈ : _<_ Respectsʳ (flip _≈_) → (Acc _<_) Respects _≈_
+
+  Acc-asymm : (x : A) → (Acc _<_ x) → (y : A) → x < y → ¬ (y < x)
+  Wf-asymm : WellFounded _<_ → Asymmetric _<_
+    
+  Acc-irrefl : {_≈_ : Rel A ℓ} → Symmetric _≈_ → _<_ Respects₂ _≈_ → 
+               (x : A) → Acc _<_ x →  (y : A) → x ≈ y → ¬ (x < y)
+  Wf-irrefl : WellFounded _<_ → {_≈_ : Rel A ℓ} → Symmetric _≈_ → 
+              _<_ Respects₂ _≈_ → Irreflexive _≈_ _<_
   ```
 
 * Added new file `Relation.Binary.Reasoning.Base.Apartness`
diff --git a/src/Induction/WellFounded.agda b/src/Induction/WellFounded.agda
index 7615c99337..6583ac554a 100644
--- a/src/Induction/WellFounded.agda
+++ b/src/Induction/WellFounded.agda
@@ -8,7 +8,7 @@
 
 module Induction.WellFounded where
 
-open import Data.Product.Base using (Σ; _,_; proj₁)
+open import Data.Product.Base using (Σ; _,_; proj₁; proj₂)
 open import Function.Base using (_∘_; flip; _on_)
 open import Induction
 open import Level using (Level; _⊔_)
@@ -17,6 +17,7 @@ open import Relation.Binary.Definitions
   using (Symmetric; _Respectsʳ_; _Respects_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 open import Relation.Unary
+open import Relation.Nullary.Negation.Core using (¬_)
 
 private
   variable
@@ -112,6 +113,24 @@ module FixPoint
   unfold-wfRec : ∀ {x} → wfRec P f x ≡ f x (λ y _ → wfRec P f y)
   unfold-wfRec {x} = f-ext x wfRecBuilder-wfRec
 
+------------------------------------------------------------------------
+-- Well-founded relations are asymmetric and irreflexive.
+
+module _ {_<_ : Rel A r} where
+  Acc-asymm : (x : A) → (Acc _<_ x) → (y : A) → x < y → ¬ (y < x)
+  Acc-asymm = Some.wfRec _ λ x hx y x<y y<x → hx y y<x x y<x x<y
+
+  Wf-asymm : WellFounded _<_ → Asymmetric _<_
+  Wf-asymm wf x<y y<x = Acc-asymm _ (wf _) _ x<y y<x
+
+  Acc-irrefl : {_≈_ : Rel A ℓ} → Symmetric _≈_ → _<_ Respects₂ _≈_ → 
+               (x : A) → Acc _<_ x →  (y : A) → x ≈ y → ¬ (x < y)
+  Acc-irrefl s r x p y x≈y x<y = 
+    Acc-asymm x p y x<y (proj₂ r x≈y (proj₁ r (s x≈y) x<y))
+
+  Wf-irrefl : WellFounded _<_ → {_≈_ : Rel A ℓ} → Symmetric _≈_ → 
+              _<_ Respects₂ _≈_ → Irreflexive _≈_ _<_
+  Wf-irrefl wf s r = Acc-irrefl s r _ (wf _) _
 
 ------------------------------------------------------------------------
 -- It might be useful to establish proofs of Acc or Well-founded using

From 935ed982ab08e72836de3748317df0089750c978 Mon Sep 17 00:00:00 2001
From: Ioannis Markakis <70938217+jmarkakis@users.noreply.github.com>
Date: Tue, 3 Oct 2023 08:41:44 +0100
Subject: [PATCH 2/5] Renamed wf-asym, acc-asym and made arguments implicit

---
 CHANGELOG.md                   |  8 ++++----
 src/Induction/WellFounded.agda | 24 +++++++++++++-----------
 2 files changed, 17 insertions(+), 15 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index ac84b7f058..9a5d9e3eea 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -3515,12 +3515,12 @@ This is a full list of proofs that have changed form to use irrelevant instance
   ```agda
   Acc-resp-flip-≈ : _<_ Respectsʳ (flip _≈_) → (Acc _<_) Respects _≈_
 
-  Acc-asymm : (x : A) → (Acc _<_ x) → (y : A) → x < y → ¬ (y < x)
-  Wf-asymm : WellFounded _<_ → Asymmetric _<_
+  acc-asym : (x : A) → Acc _<_ x → (y : A) → x < y → ¬ (y < x)
+  wf-asym : WellFounded _<_ → Asymmetric _<_
     
-  Acc-irrefl : {_≈_ : Rel A ℓ} → Symmetric _≈_ → _<_ Respects₂ _≈_ → 
+  acc-irrefl : {_≈_ : Rel A ℓ} → Symmetric _≈_ → _<_ Respects₂ _≈_ → 
                (x : A) → Acc _<_ x →  (y : A) → x ≈ y → ¬ (x < y)
-  Wf-irrefl : WellFounded _<_ → {_≈_ : Rel A ℓ} → Symmetric _≈_ → 
+  wf-irrefl : WellFounded _<_ → {_≈_ : Rel A ℓ} → Symmetric _≈_ → 
               _<_ Respects₂ _≈_ → Irreflexive _≈_ _<_
   ```
 
diff --git a/src/Induction/WellFounded.agda b/src/Induction/WellFounded.agda
index 6583ac554a..4dac202efb 100644
--- a/src/Induction/WellFounded.agda
+++ b/src/Induction/WellFounded.agda
@@ -14,7 +14,8 @@ open import Induction
 open import Level using (Level; _⊔_)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions
-  using (Symmetric; _Respectsʳ_; _Respects_)
+  using (Symmetric; Asymmetric; Irreflexive; _Respects₂_; 
+    _Respectsʳ_; _Respects_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 open import Relation.Unary
 open import Relation.Nullary.Negation.Core using (¬_)
@@ -117,20 +118,21 @@ module FixPoint
 -- Well-founded relations are asymmetric and irreflexive.
 
 module _ {_<_ : Rel A r} where
-  Acc-asymm : (x : A) → (Acc _<_ x) → (y : A) → x < y → ¬ (y < x)
-  Acc-asymm = Some.wfRec _ λ x hx y x<y y<x → hx y y<x x y<x x<y
+  acc-asym : ∀ {x y} → (Acc _<_ x) → x < y → ¬ (y < x)
+  acc-asym {x} {y} hx = 
+    (Some.wfRec _ λ x hx y x<y y<x → hx y y<x x y<x x<y) x hx y
 
-  Wf-asymm : WellFounded _<_ → Asymmetric _<_
-  Wf-asymm wf x<y y<x = Acc-asymm _ (wf _) _ x<y y<x
+  wf-asym : WellFounded _<_ → Asymmetric _<_
+  wf-asym wf = acc-asym (wf _)
 
-  Acc-irrefl : {_≈_ : Rel A ℓ} → Symmetric _≈_ → _<_ Respects₂ _≈_ → 
-               (x : A) → Acc _<_ x →  (y : A) → x ≈ y → ¬ (x < y)
-  Acc-irrefl s r x p y x≈y x<y = 
-    Acc-asymm x p y x<y (proj₂ r x≈y (proj₁ r (s x≈y) x<y))
+  acc-irrefl : {_≈_ : Rel A ℓ} → Symmetric _≈_ → _<_ Respects₂ _≈_ → 
+               ∀ {x y} → Acc _<_ x → x ≈ y → ¬ (x < y)
+  acc-irrefl s r {x} {y} hx x≈y x<y = 
+    acc-asym hx x<y (proj₂ r x≈y (proj₁ r (s x≈y) x<y))
 
-  Wf-irrefl : WellFounded _<_ → {_≈_ : Rel A ℓ} → Symmetric _≈_ → 
+  wf-irrefl : WellFounded _<_ → {_≈_ : Rel A ℓ} → Symmetric _≈_ → 
               _<_ Respects₂ _≈_ → Irreflexive _≈_ _<_
-  Wf-irrefl wf s r = Acc-irrefl s r _ (wf _) _
+  wf-irrefl wf s r = acc-irrefl s r (wf _)
 
 ------------------------------------------------------------------------
 -- It might be useful to establish proofs of Acc or Well-founded using

From 041318029cc87212e830618209eebedbdb59dd74 Mon Sep 17 00:00:00 2001
From: Ioannis Markakis <70938217+jmarkakis@users.noreply.github.com>
Date: Tue, 3 Oct 2023 09:51:31 +0100
Subject: [PATCH 3/5] Simplified wf-irrefl, and changed CHANGElOG

---
 CHANGELOG.md                   |  8 +++-----
 src/Induction/WellFounded.agda | 14 +++++---------
 2 files changed, 8 insertions(+), 14 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9a5d9e3eea..3230bf553b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -3515,13 +3515,11 @@ This is a full list of proofs that have changed form to use irrelevant instance
   ```agda
   Acc-resp-flip-≈ : _<_ Respectsʳ (flip _≈_) → (Acc _<_) Respects _≈_
 
-  acc-asym : (x : A) → Acc _<_ x → (y : A) → x < y → ¬ (y < x)
+  acc-asym : ∀ {x y} → Acc _<_ x → x < y → ¬ (y < x)
   wf-asym : WellFounded _<_ → Asymmetric _<_
     
-  acc-irrefl : {_≈_ : Rel A ℓ} → Symmetric _≈_ → _<_ Respects₂ _≈_ → 
-               (x : A) → Acc _<_ x →  (y : A) → x ≈ y → ¬ (x < y)
-  wf-irrefl : WellFounded _<_ → {_≈_ : Rel A ℓ} → Symmetric _≈_ → 
-              _<_ Respects₂ _≈_ → Irreflexive _≈_ _<_
+  wf-irrefl : {_≈_ : Rel A ℓ} → _<_ Respects₂ _≈_ → 
+              Symmetric _≈_ → WellFounded _<_ → Irreflexive _≈_ _<_
   ```
 
 * Added new file `Relation.Binary.Reasoning.Base.Apartness`
diff --git a/src/Induction/WellFounded.agda b/src/Induction/WellFounded.agda
index 4dac202efb..61fc362be4 100644
--- a/src/Induction/WellFounded.agda
+++ b/src/Induction/WellFounded.agda
@@ -17,6 +17,7 @@ open import Relation.Binary.Definitions
   using (Symmetric; Asymmetric; Irreflexive; _Respects₂_; 
     _Respectsʳ_; _Respects_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
+open import Relation.Binary.Consequences using (asym⇒irr)
 open import Relation.Unary
 open import Relation.Nullary.Negation.Core using (¬_)
 
@@ -118,21 +119,16 @@ module FixPoint
 -- Well-founded relations are asymmetric and irreflexive.
 
 module _ {_<_ : Rel A r} where
-  acc-asym : ∀ {x y} → (Acc _<_ x) → x < y → ¬ (y < x)
+  acc-asym : ∀ {x y} → Acc _<_ x → x < y → ¬ (y < x)
   acc-asym {x} {y} hx = 
     (Some.wfRec _ λ x hx y x<y y<x → hx y y<x x y<x x<y) x hx y
 
   wf-asym : WellFounded _<_ → Asymmetric _<_
   wf-asym wf = acc-asym (wf _)
 
-  acc-irrefl : {_≈_ : Rel A ℓ} → Symmetric _≈_ → _<_ Respects₂ _≈_ → 
-               ∀ {x y} → Acc _<_ x → x ≈ y → ¬ (x < y)
-  acc-irrefl s r {x} {y} hx x≈y x<y = 
-    acc-asym hx x<y (proj₂ r x≈y (proj₁ r (s x≈y) x<y))
-
-  wf-irrefl : WellFounded _<_ → {_≈_ : Rel A ℓ} → Symmetric _≈_ → 
-              _<_ Respects₂ _≈_ → Irreflexive _≈_ _<_
-  wf-irrefl wf s r = acc-irrefl s r (wf _)
+  wf-irrefl : {_≈_ : Rel A ℓ} → _<_ Respects₂ _≈_ → 
+              Symmetric _≈_ → WellFounded _<_ → Irreflexive _≈_ _<_
+  wf-irrefl r s wf = asym⇒irr r s (wf-asym wf)
 
 ------------------------------------------------------------------------
 -- It might be useful to establish proofs of Acc or Well-founded using

From 43f917843b0e5608e50d0aadd9f572cf4c66811a Mon Sep 17 00:00:00 2001
From: Ioannis Markakis <70938217+jmarkakis@users.noreply.github.com>
Date: Tue, 3 Oct 2023 12:27:57 +0100
Subject: [PATCH 4/5] Update CHANGELOG.md

---
 CHANGELOG.md | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3230bf553b..f200b3a0de 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -3515,11 +3515,10 @@ This is a full list of proofs that have changed form to use irrelevant instance
   ```agda
   Acc-resp-flip-≈ : _<_ Respectsʳ (flip _≈_) → (Acc _<_) Respects _≈_
 
-  acc-asym : ∀ {x y} → Acc _<_ x → x < y → ¬ (y < x)
+  acc-asym : Acc _<_ x → x < y → ¬ (y < x)
   wf-asym : WellFounded _<_ → Asymmetric _<_
-    
-  wf-irrefl : {_≈_ : Rel A ℓ} → _<_ Respects₂ _≈_ → 
-              Symmetric _≈_ → WellFounded _<_ → Irreflexive _≈_ _<_
+  wf-irrefl : _<_ Respects₂ _≈_ → Symmetric _≈_ →
+              WellFounded _<_ → Irreflexive _≈_ _<_
   ```
 
 * Added new file `Relation.Binary.Reasoning.Base.Apartness`

From 285902acd6437bc65f888072f68e6386a5a39b64 Mon Sep 17 00:00:00 2001
From: Ioannis Markakis <70938217+jmarkakis@users.noreply.github.com>
Date: Thu, 5 Oct 2023 13:26:32 +0100
Subject: [PATCH 5/5] Changed names + solved a merge conflict

---
 CHANGELOG.md                   |  6 +++---
 src/Induction/WellFounded.agda | 14 +++++++-------
 2 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index af0243741a..a378ec3c56 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -3746,9 +3746,9 @@ This is a full list of proofs that have changed form to use irrelevant instance
   ```agda
   Acc-resp-flip-≈ : _<_ Respectsʳ (flip _≈_) → (Acc _<_) Respects _≈_
 
-  acc-asym : Acc _<_ x → x < y → ¬ (y < x)
-  wf-asym : WellFounded _<_ → Asymmetric _<_
-  wf-irrefl : _<_ Respects₂ _≈_ → Symmetric _≈_ →
+  acc⇒asym : Acc _<_ x → x < y → ¬ (y < x)
+  wf⇒asym : WellFounded _<_ → Asymmetric _<_
+  wf⇒irrefl : _<_ Respects₂ _≈_ → Symmetric _≈_ →
               WellFounded _<_ → Irreflexive _≈_ _<_
   ```
 
diff --git a/src/Induction/WellFounded.agda b/src/Induction/WellFounded.agda
index 7f1b62a708..fb3ed14255 100644
--- a/src/Induction/WellFounded.agda
+++ b/src/Induction/WellFounded.agda
@@ -123,16 +123,16 @@ module FixPoint
 -- Well-founded relations are asymmetric and irreflexive.
 
 module _ {_<_ : Rel A r} where
-  acc-asym : ∀ {x y} → Acc _<_ x → x < y → ¬ (y < x)
-  acc-asym {x} {y} hx = 
-    (Some.wfRec _ λ x hx y x<y y<x → hx y y<x x y<x x<y) x hx y
+  acc⇒asym : ∀ {x y} → Acc _<_ x → x < y → ¬ (y < x)
+  acc⇒asym {x} hx =
+    Some.wfRec (λ x → ∀ {y} → x < y → ¬ (y < x)) (λ _ hx x<y y<x → hx y<x y<x x<y) _ hx
 
-  wf-asym : WellFounded _<_ → Asymmetric _<_
-  wf-asym wf = acc-asym (wf _)
+  wf⇒asym : WellFounded _<_ → Asymmetric _<_
+  wf⇒asym wf = acc⇒asym (wf _)
 
-  wf-irrefl : {_≈_ : Rel A ℓ} → _<_ Respects₂ _≈_ → 
+  wf⇒irrefl : {_≈_ : Rel A ℓ} → _<_ Respects₂ _≈_ → 
               Symmetric _≈_ → WellFounded _<_ → Irreflexive _≈_ _<_
-  wf-irrefl r s wf = asym⇒irr r s (wf-asym wf)
+  wf⇒irrefl r s wf = asym⇒irr r s (wf⇒asym wf)
 
 ------------------------------------------------------------------------
 -- It might be useful to establish proofs of Acc or Well-founded using