feat(Data/Seq): structural lemmas (leanprover-community#19859)

* Add several theorems about `Stream'.Seq`, mainly on sequence operations with `nil` and `cons`.  
* Introduce the `fold` operation for sequences and prove a few structural lemmas about it.
* Rename `Seq.destruct_eq_nil` as `Seq.destruct_eq_none`.

Author: vasnesterov

Mathlib/Data/Seq/Parallel.lean

@@ -166,7 +166,7 @@ theorem terminates_parallel {S : WSeq (Computation α)} {c} (h : c ∈ S) [T : T
         rw [D]
         simp only
         have TT := TT l'
-        rwa [Seq.destruct_eq_nil D, Seq.tail_nil] at TT
+        rwa [Seq.destruct_eq_none D, Seq.tail_nil] at TT
       · have D : Seq.destruct S = some (o, S.tail) := by
           dsimp [Seq.destruct]
           rw [e]