diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index e181a291e9..cd30778f12 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -955,7 +955,7 @@ private
 -- then we can find the smallest value for which this is the case.
 
 ¬∀⟶∃¬-smallest : ∀ n {p} (P : Pred (Fin n) p) → Decidable P →
-                 ¬ (∀ i → P i) → ∃ λ i → ¬ P i × ((j : Fin′ i) → P (inject j))
+                 ¬ (∀ i → P i) → ∃ λ i → (¬ P i) × ((j : Fin′ i) → P (inject j))
 ¬∀⟶∃¬-smallest zero    P P? ¬∀P = contradiction (λ()) ¬∀P
 ¬∀⟶∃¬-smallest (suc n) P P? ¬∀P with P? zero
 ... | false because [¬P₀] = (zero , invert [¬P₀] , λ ())
diff --git a/src/Data/List/Relation/Binary/Sublist/Setoid.agda b/src/Data/List/Relation/Binary/Sublist/Setoid.agda
index 8915308cf2..b48bc60f47 100644
--- a/src/Data/List/Relation/Binary/Sublist/Setoid.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Setoid.agda
@@ -44,7 +44,7 @@ _⊇_ : Rel (List A) (c ⊔ ℓ)
 xs ⊇ ys = ys ⊆ xs
 
 _⊂_ : Rel (List A) (c ⊔ ℓ)
-xs ⊂ ys = xs ⊆ ys × ¬ (xs ≋ ys)
+xs ⊂ ys = xs ⊆ ys × (¬ (xs ≋ ys))
 
 _⊃_ : Rel (List A) (c ⊔ ℓ)
 xs ⊃ ys = ys ⊂ xs
diff --git a/src/Relation/Nullary/Negation/Core.agda b/src/Relation/Nullary/Negation/Core.agda
index 5c4efaf4fb..29dc7f37f4 100644
--- a/src/Relation/Nullary/Negation/Core.agda
+++ b/src/Relation/Nullary/Negation/Core.agda
@@ -27,7 +27,7 @@ private
 ------------------------------------------------------------------------
 -- Negation.
 
-infix 3 ¬_
+infix 1.5 ¬_
 ¬_ : Set a → Set a
 ¬ P = P → ⊥