Fixed Data.Nat.Binary.Properties propertis

Author: MatthewDaggitt

src/Data/List/Relation/Binary/Sublist/Propositional/Example/UniqueBoundVariables.agda

@@ -14,8 +14,8 @@ open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; cong;
 open ≡-Reasoning
 
 open import Data.List using (List; []; _∷_; [_])
-open import Data.List.All using (Null; [])
 open import Data.List.Membership.Propositional using (_∈_)
+open import Data.List.Relation.Unary.All using (Null; [])
 open import Data.List.Relation.Binary.Sublist.Propositional using
   ( _⊆_; []; _∷_; _∷ʳ_
   ; ⊆-refl; ⊆-trans; minimum

src/Data/Nat/Binary/Properties.agda

@@ -778,14 +778,14 @@ private
 +-monoʳ-< :  ∀ x → (x +_) Preserves _<_ ⟶ _<_
 +-monoʳ-< x y<z =  +-mono-≤-< (≤-refl {x}) y<z
 
-x≤y+x :  ∀ (x y) → x ≤ y + x
+x≤y+x :  ∀ x y → x ≤ y + x
 x≤y+x x y =  begin
   x        ≡⟨ sym (+-identityˡ x) ⟩
   0ᵇ + x   ≤⟨ +-monoˡ-≤ x (0≤x y) ⟩
   y + x    ∎
   where open ≤-Reasoning
 
-x≤x+y :  ∀ (x y) → x ≤ x + y
+x≤x+y :  ∀ x y → x ≤ x + y
 x≤x+y x y =  begin
   x        ≤⟨ x≤y+x x y ⟩
   y + x    ≡⟨ +-comm y x ⟩
@@ -1318,7 +1318,7 @@ suc-* x y = begin
   x + x * y    ∎
   where open ≡-Reasoning
 
-x≤suc[y]*x :  ∀ (x y) → x ≤ (suc y) * x
+x≤suc[y]*x :  ∀ x y → x ≤ (suc y) * x
 x≤suc[y]*x x y =  begin
   x             ≤⟨ x≤x+y x (y * x) ⟩
   x + y * x     ≡⟨ sym (suc-* y x) ⟩