Improve Data.List.Base.unfold (#2359; deprecate use of with #2123) (

#2364)

* `with`-free definition of `unfold`

* fixed previous commit

src/Data/List/Base.agda

@@ -250,9 +250,7 @@ unfold : ∀ (P : ℕ → Set b)
  (f : ∀ {n} → P (suc n) → Maybe (A × P n)) →
  ∀ {n} → P n → List A
 unfold P f {n = zero} s = []
-unfold P f {n = suc n} s with f s
-... | nothing = []
-... | just (x , s′) = x ∷ unfold P f s′
+unfold P f {n = suc n} s = maybe′ (λ (x , s′) → x ∷ unfold P f s′) [] (f s)
 
 ------------------------------------------------------------------------
 -- Operations for reversing lists