Add keep and drop to subsets over lists (#1459)

Author: Carlos Tomé

CHANGELOG.md

@@ -483,11 +483,15 @@ Other minor additions
 
 * Added new proof to `Data.List.Relation.Binary.Subset.Setoid.Properties`:
   ```agda
+  xs⊆x∷xs    : xs ⊆ x ∷ xs
+  ∷⁺ʳ        : xs ⊆ ys → x ∷ xs ⊆ x ∷ ys
   applyUpTo⁺ : m ≤ n → applyUpTo f m ⊆ applyUpTo f n
   ```
 
 * Added new proof to `Data.List.Relation.Binary.Subset.Propositional.Properties`:
   ```agda
+  xs⊆x∷xs    : xs ⊆ x ∷ xs
+  ∷⁺ʳ        : xs ⊆ ys → x ∷ xs ⊆ x ∷ ys
   applyUpTo⁺ : m ≤ n → applyUpTo f m ⊆ applyUpTo f n
   ```
 

src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda

@@ -133,6 +133,15 @@ map⁺ f xs⊆ys =
   Prod.map₂ (Prod.map₁ xs⊆ys) ∘
   _⟨$⟩_ (Inverse.from (map-∈↔ f))
 
+------------------------------------------------------------------------
+-- ∷
+
+xs⊆x∷xs : ∀ (xs : List A) x → xs ⊆ x ∷ xs
+xs⊆x∷xs = Setoidₚ.xs⊆x∷xs (setoid _)
+
+∷⁺ʳ : ∀ x → xs ⊆ ys → x ∷ xs ⊆ x ∷ ys
+∷⁺ʳ = Setoidₚ.∷⁺ʳ (setoid _)
+
 ------------------------------------------------------------------------
 -- _++_
 

src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda

@@ -171,6 +171,19 @@ module _ (S : Setoid a ℓ) where
 ------------------------------------------------------------------------
 -- Properties of list functions
 ------------------------------------------------------------------------
+-- ∷
+
+module _ (S : Setoid a ℓ) where
+
+  open Subset S
+
+  xs⊆x∷xs : ∀ xs x → xs ⊆ x ∷ xs
+  xs⊆x∷xs xs x = there
+
+  ∷⁺ʳ : ∀ {xs ys} x → xs ⊆ ys → x ∷ xs ⊆ x ∷ ys
+  ∷⁺ʳ x xs⊆ys (here  p) = here p
+  ∷⁺ʳ x xs⊆ys (there p) = there (xs⊆ys p)
+
 -- ++
 
 module _ (S : Setoid a ℓ) where