-- Lean 4 proof step from Mathlib.Data.Seq.Parallel (goal)
Goal:
α : Type u
β : Type v
f : α → β
S_1 : WSeq (Computation α)
c1 c2 : Computation β
h :
  ∃ (l : List (Computation α)) (S : WSeq (Computation α)),
    c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH :
  Eq (α := β ⊕ List (Computation β))
    (List.foldr
      (fun (c : Computation β) (o : β ⊕ List (Computation β)) ↦
        match (motive := β ⊕ List (Computation β) → β ⊕ List (Computation β)) o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match (motive := β ⊕ Computation β → β ⊕ List (Computation β)) c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) (List.map (map f) l))
    (match (motive := Sum.{u, v} α (List (Computation β)) → β ⊕ List (Computation β))
      match (motive := α ⊕ List (Computation α) → Sum.{u, v} α (List (Computation β)))
        List.foldr
          (fun (c : Computation α) (o : α ⊕ List (Computation α)) ↦
            match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) o with
            | Sum.inl a => Sum.inl a
            | Sum.inr ls =>
              match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
              | Sum.inl a => Sum.inl a
              | Sum.inr b => Sum.inr (b :: ls))
          (Sum.inr []) l with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (List.map (map f) b) with
    | Sum.inl a => Sum.inl (f a)
    | Sum.inr b => Sum.inr b)
⊢ Eq (α := β ⊕ List (Computation β))
    (match (motive := β ⊕ List (Computation β) → β ⊕ List (Computation β))
        List.foldr
          (fun (c : Computation β) (o : β ⊕ List (Computation β)) ↦
            match (motive := β ⊕ List (Computation β) → β ⊕ List (Computation β)) o with
            | Sum.inl a => Sum.inl a
            | Sum.inr ls =>
              match (motive := β ⊕ Computation β → β ⊕ List (Computation β)) c.destruct with
              | Sum.inl a => Sum.inl a
              | Sum.inr b => Sum.inr (b :: ls))
          (Sum.inr []) (List.map (map f) l) with
      | Sum.inl a => Sum.inl a
      | Sum.inr ls =>
        match (motive := β ⊕ Computation β → β ⊕ List (Computation β))
          match (motive := Sum.{u, v} α (Computation β) → β ⊕ Computation β)
            match (motive := α ⊕ Computation α → Sum.{u, v} α (Computation β)) c.destruct with
            | Sum.inl a => Sum.inl a
            | Sum.inr b => Sum.inr (map f b) with
          | Sum.inl a => Sum.inl (f a)
          | Sum.inr b => Sum.inr b with
        | Sum.inl a => Sum.inl a
        | Sum.inr b => Sum.inr (b :: ls) :
      β ⊕ List (Computation β))
    (match (motive := Sum.{u, v} α (List (Computation β)) → β ⊕ List (Computation β))
        match (motive := α ⊕ List (Computation α) → Sum.{u, v} α (List (Computation β)))
          match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α))
            List.foldr
              (fun (c : Computation α) (o : α ⊕ List (Computation α)) ↦
                match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) o with
                | Sum.inl a => Sum.inl a
                | Sum.inr ls =>
                  match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
                  | Sum.inl a => Sum.inl a
                  | Sum.inr b => Sum.inr (b :: ls))
              (Sum.inr []) l with
          | Sum.inl a => Sum.inl a
          | Sum.inr ls =>
            match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
            | Sum.inl a => Sum.inl a
            | Sum.inr b => Sum.inr (b :: ls) with
        | Sum.inl a => Sum.inl a
        | Sum.inr b => Sum.inr (List.map (map f) b) with
      | Sum.inl a => Sum.inl (f a)
      | Sum.inr b => Sum.inr b :
      β ⊕ List (Computation β))
have cons : Eq.{v + 1} (α := β ⊕ List (Computation β))
  (match (motive := β ⊕ List (Computation β) → β ⊕ List (Computation β))
      match (motive := Sum.{u, v} α (List (Computation β)) → β ⊕ List (Computation β))
        match (motive := α ⊕ List (Computation α) → Sum.{u, v} α (List (Computation β)))
          List.foldr
            (fun (c : Computation α) (o : α ⊕ List (Computation α)) ↦
              match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) o with
              | Sum.inl a => Sum.inl a
              | Sum.inr ls =>
                match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
                | Sum.inl a => Sum.inl a
                | Sum.inr b => Sum.inr (b :: ls))
            (Sum.inr []) l with
        | Sum.inl a => Sum.inl a
        | Sum.inr b => Sum.inr (List.map (map f) b) with
      | Sum.inl a => Sum.inl (f a)
      | Sum.inr b => Sum.inr b with
    | Sum.inl a => Sum.inl a
    | Sum.inr ls =>
      match (motive := β ⊕ Computation β → β ⊕ List (Computation β))
        match (motive := Sum.{u, v} α (Computation β) → β ⊕ Computation β)
          match (motive := α ⊕ Computation α → Sum.{u, v} α (Computation β)) c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (map f b) with
        | Sum.inl a => Sum.inl (f a)
        | Sum.inr b => Sum.inr b with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (b :: ls) :
    β ⊕ List (Computation β))
  (match (motive := Sum.{u, v} α (List (Computation β)) → β ⊕ List (Computation β))
      match (motive := α ⊕ List (Computation α) → Sum.{u, v} α (List (Computation β)))
        match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α))
          List.foldr
            (fun (c : Computation α) (o : α ⊕ List (Computation α)) ↦
              match (motive := α ⊕ List (Computation α) → α ⊕ List (Computation α)) o with
              | Sum.inl a => Sum.inl a
              | Sum.inr ls =>
                match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
                | Sum.inl a => Sum.inl a
                | Sum.inr b => Sum.inr (b :: ls))
            (Sum.inr []) l with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls) with
      | Sum.inl a => Sum.inl a
      | Sum.inr b => Sum.inr (List.map (map f) b) with
    | Sum.inl a => Sum.inl (f a)
    | Sum.inr b => Sum.inr b :
    β ⊕ List (Computation β))
Tactic: rw [IH]