Add all⊆concat (agda#2513)

* Fixes agda#2509

* remove parentheses

Author: jamesmckinna

CHANGELOG.md

@@ -315,6 +315,11 @@ Additions to existing modules
                                             ([] , [])
   ```
 
+* In `Data.List.Relation.Unary.All.Properties`:
+  ```agda
+  all⊆concat : (xss : List (List A)) → All (Sublist._⊆ concat xss) xss
+  ```
+
 * In `Data.List.Relation.Unary.Any.Properties`:
   ```agda
   concatMap⁺ : Any (Any P ∘ f) xs → Any P (concatMap f xs)

src/Data/List/Relation/Unary/All/Properties.agda

@@ -20,7 +20,10 @@ import Data.List.Membership.Setoid as SetoidMembership
 import Data.List.Properties as List
 import Data.List.Relation.Binary.Equality.Setoid as ≋
 open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; []; _∷_)
-open import Data.List.Relation.Binary.Subset.Propositional using (_⊆_)
+import Data.List.Relation.Binary.Sublist.Propositional as Sublist
+import Data.List.Relation.Binary.Sublist.Propositional.Properties
+  as Sublist
+import Data.List.Relation.Binary.Subset.Propositional as Subset
 open import Data.List.Relation.Unary.All as All using
   ( All; []; _∷_; lookup; updateAt
   ; _[_]=_; here; there
@@ -385,6 +388,11 @@ concat⁻ : ∀ {xss} → All P (concat xss) → All (All P) xss
 concat⁻ {xss = []}       []  = []
 concat⁻ {xss = xs ∷ xss} pxs = ++⁻ˡ xs pxs ∷ concat⁻ (++⁻ʳ xs pxs)
 
+all⊆concat : (xss : List (List A)) → All (Sublist._⊆ concat xss) xss
+all⊆concat [] = []
+all⊆concat (xs ∷ xss) =
+  Sublist.++⁺ʳ (concat xss) Sublist.⊆-refl ∷ All.map (Sublist.++⁺ˡ xs) (all⊆concat xss)
+
 ------------------------------------------------------------------------
 -- snoc
 
@@ -675,10 +683,10 @@ module _ (p : A → Bool) where
 ------------------------------------------------------------------------
 -- All is anti-monotone.
 
-anti-mono : xs ⊆ ys → All P ys → All P xs
+anti-mono : xs Subset.⊆ ys → All P ys → All P xs
 anti-mono xs⊆ys pys = All.tabulate (lookup pys ∘ xs⊆ys)
 
-all-anti-mono : ∀ (p : A → Bool) → xs ⊆ ys → T (all p ys) → T (all p xs)
+all-anti-mono : ∀ (p : A → Bool) → xs Subset.⊆ ys → T (all p ys) → T (all p xs)
 all-anti-mono p xs⊆ys = all⁻ p ∘ anti-mono xs⊆ys ∘ all⁺ p _
 
 ------------------------------------------------------------------------