diff --git a/CHANGELOG.md b/CHANGELOG.md
index 812fe00b6c..f9dfd695ad 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2929,6 +2929,13 @@ Other minor changes
                     f Preserves₂ ≈₁ ⟶ ≈₁ ⟶ ≈₂
   ```
 
+* Added new proofs to `Relation.Binary.Construct.Closure.Transitive`:
+  ```
+  accessible⁻ : ∀ {x} → Acc _∼⁺_ x → Acc _∼_ x
+  wellFounded⁻ : WellFounded _∼⁺_ → WellFounded _∼_
+  accessible : ∀ {x} → Acc _∼_ x → Acc _∼⁺_ x
+  ```
+
 * Added new operations in `Relation.Binary.PropositionalEquality.Properties`:
   ```
   J       : (B : (y : A) → x ≡ y → Set b) (p : x ≡ y) → B x refl → B y p
diff --git a/src/Relation/Binary/Construct/Closure/Transitive.agda b/src/Relation/Binary/Construct/Closure/Transitive.agda
index ed20e48bb0..7c12fa7bcd 100644
--- a/src/Relation/Binary/Construct/Closure/Transitive.agda
+++ b/src/Relation/Binary/Construct/Closure/Transitive.agda
@@ -58,6 +58,7 @@ module _ {_∼_ : Rel A ℓ} where
 module _ (_∼_ : Rel A ℓ) where
   private
     _∼⁺_ = TransClosure _∼_
+    module ∼⊆∼⁺ = Subrelation {_<₂_ = _∼⁺_} [_]
 
   reflexive : Reflexive _∼_ → Reflexive _∼⁺_
   reflexive refl = [ refl ]
@@ -69,17 +70,21 @@ module _ (_∼_ : Rel A ℓ) where
   transitive : Transitive _∼⁺_
   transitive = _++_
 
-  wellFounded : WellFounded _∼_ → WellFounded _∼⁺_
-  wellFounded wf = λ x → acc (accessible′ (wf x))
-    where
-    downwardsClosed : ∀ {x y} → Acc _∼⁺_ y → x ∼ y → Acc _∼⁺_ x
-    downwardsClosed (acc rec) x∼y = acc (λ z z∼x → rec z (z∼x ∷ʳ x∼y))
+  accessible⁻ : ∀ {x} → Acc _∼⁺_ x → Acc _∼_ x
+  accessible⁻ = ∼⊆∼⁺.accessible
 
-    accessible′ : ∀ {x} → Acc _∼_ x → WfRec _∼⁺_ (Acc _∼⁺_) x
-    accessible′ (acc rec) y [ y∼x ]      = acc (accessible′ (rec y y∼x))
-    accessible′ acc[x]    y (y∼z ∷ z∼⁺x) =
-      downwardsClosed (accessible′ acc[x] _ z∼⁺x) y∼z
+  wellFounded⁻ : WellFounded _∼⁺_ → WellFounded _∼_
+  wellFounded⁻ = ∼⊆∼⁺.wellFounded
 
+  accessible : ∀ {x} → Acc _∼_ x → Acc _∼⁺_ x
+  accessible acc[x] = acc (wf-acc acc[x])
+    where
+    wf-acc : ∀ {x} → Acc _∼_ x → WfRec _∼⁺_ (Acc _∼⁺_) x
+    wf-acc (acc rec) _ [ y∼x ]   = acc (wf-acc (rec _ y∼x))
+    wf-acc acc[x] _ (y∼z ∷ z∼⁺x) = acc-inverse (wf-acc acc[x] _ z∼⁺x) _ [ y∼z ]
+
+  wellFounded : WellFounded _∼_ → WellFounded _∼⁺_
+  wellFounded wf x = accessible (wf x)
 
 
 ------------------------------------------------------------------------