some cleanup

agda · Feb 6, 2024 · 88c23b0 · 88c23b0
1 parent 51e1b29
commit 88c23b0
Showing 1 changed file with 0 additions and 3 deletions.
diff --git a/Cubical/Foundations/Powerset.agda b/Cubical/Foundations/Powerset.agda
@@ -50,9 +50,6 @@ A ⊆ B = ∀ x → x ∈ A → x ∈ B
 subst-∈ : (A : ℙ X) {x y : X} → x ≡ y → x ∈ A → y ∈ A
 subst-∈ A = subst (_∈ A)
 
-subst-∈' : (A : ℙ X) {x y : X} → x ∈ A → x ≡ y  → y ∈ A
-subst-∈' A x p = subst (_∈ A) p x
-
 ⊆-refl-consequence : (A B : ℙ X) → A ≡ B → (A ⊆ B) × (B ⊆ A)
 ⊆-refl-consequence A B p = subst (A ⊆_) p (⊆-refl A)
                          , subst (B ⊆_) (sym p) (⊆-refl B)