-- 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)
val : List (Computation α)
⊢ 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 β))) Sum.inr val 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 α)) Sum.inr val 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 : ∀ (val_1 : α),
  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 β))) Sum.inr val 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 β)) Sum.inl val_1 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 α)) Sum.inr val with
          | Sum.inl a => Sum.inl a
          | Sum.inr ls =>
            match (motive := α ⊕ Computation α → α ⊕ List (Computation α)) Sum.inl val_1 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: cases destruct c