∀ {α : Type u} (l : List (Computation α)) (S : Stream'.WSeq (Computation α)),
  Computation.parallel.aux1✝ (l, S) =
    Computation.rmap
      (fun l' =>
        match Stream'.Seq.destruct S with
        | none => (l', Stream'.Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))
      (Computation.parallel.aux2✝ l)