fixed issue #602 for vectors, too (#1672)

Author: jamesmckinna

CHANGELOG.md

@@ -1014,6 +1014,11 @@ Other minor changes
   transpose-replicate : transpose (replicate xs) ≡ map replicate xs
   ```
 
+* Added new proofs in `Data.Vec.Relation.Binary.Lex.Strict`:
+  ```agda
+  xs≮[] : ∀ {n} (xs : Vec A n) → ¬ xs < []
+  ```
+
 * Added new functions in `Data.Vec.Relation.Unary.All`:
   ```
   decide :  Π[ P ∪ Q ] → Π[ All P ∪ Any Q ]

src/Data/Vec/Relation/Binary/Lex/Strict.agda

@@ -60,8 +60,11 @@ module _ {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where
     _≋_ = Pointwise _≈_
     _<_ = Lex-< _≈_ _≺_
 
+  xs≮[] : ∀ {n} (xs : Vec A n) → ¬ xs < []
+  xs≮[] _ (base ())
+
   ¬[]<[] : ¬ [] < []
-  ¬[]<[] (base ())
+  ¬[]<[] = xs≮[] []
 
   module _ (≺-irrefl : Irreflexive _≈_ _≺_) where