add ¬First⇒All lemma to Data.List.Relation.Unary.First.Properties (agda#2507)

* add `¬First⇒All` lemma to `Data.List.Relation.Unary.First.Properties`

* Make the list argument implicit

Author: wasabi315

CHANGELOG.md

@@ -417,3 +417,9 @@ Additions to existing modules
   does-≐ : P ≐ Q → (P? : Decidable P) → (Q? : Decidable Q) → does ∘ P? ≗ does ∘ Q?
   does-≡ : (P? P?′ : Decidable P) → does ∘ P? ≗ does ∘ P?′
   ```
+
+* In `Data.List.Relation.Unary.First.Properties`:
+  ```agda
+  ¬First⇒All : ∁ Q ⊆ P → ∁ (First P Q) ⊆ All P
+  ```
+

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

@@ -59,6 +59,12 @@ module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} where
   First⇒¬All q⇒¬p [ qx ]     (px ∷ pxs) = q⇒¬p qx px
   First⇒¬All q⇒¬p (_ ∷ pqxs) (_ ∷ pxs)  = First⇒¬All q⇒¬p pqxs pxs
 
+  ¬First⇒All : ∁ Q ⊆ P → ∁ (First P Q) ⊆ All P
+  ¬First⇒All ¬q⇒p {[]}     _      = []
+  ¬First⇒All ¬q⇒p {x ∷ xs} ¬pqxxs =
+    let px = ¬q⇒p (¬pqxxs ∘ [_]) in
+    px ∷ ¬First⇒All ¬q⇒p (¬pqxxs ∘ (px ∷_))
+
 ------------------------------------------------------------------------
 -- Irrelevance