-- Lean 4 proof step from Mathlib.Data.WSeq.Defs (goal)
Goal:
α : Type u
s_1 : WSeq α
s1 s2 : Computation ℕ
l : List α
s : WSeq α
h :
  s1 =
      Computation.corec
        (fun (x : ℕ × WSeq α) ↦
          match (motive := ℕ × WSeq α → ℕ ⊕ ℕ × WSeq α) x with
          | (n, s) =>
            match (motive := Option (Seq1 (Option α)) → ℕ ⊕ ℕ × WSeq α) Seq.destruct s with
            | none => Sum.inl n
            | some (none, s') => Sum.inr (n, s')
            | some (some val, s') => Sum.inr (n + 1, s'))
        (l.length, s) ∧
    s2 =
      Computation.map (α := List α) List.length
        (Computation.corec
          (fun (x : List α × WSeq α) ↦
            match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
            | (l, s) =>
              match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l, s))
nil :
  ∀
    (h :
      s1 =
          Computation.corec
            (fun (x : ℕ × WSeq α) ↦
              match (motive := ℕ × WSeq α → ℕ ⊕ ℕ × WSeq α) x with
              | (n, s) =>
                match (motive := Option (Seq1 (Option α)) → ℕ ⊕ ℕ × WSeq α) Seq.destruct s with
                | none => Sum.inl n
                | some (none, s') => Sum.inr (n, s')
                | some (some val, s') => Sum.inr (n + 1, s'))
            (l.length, WSeq.nil) ∧
        s2 =
          Computation.map (α := List α) List.length
            (Computation.corec
              (fun (x : List α × WSeq α) ↦
                match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
                | (l, s) =>
                  match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
                  | none => Sum.inl l.reverse
                  | some (none, s') => Sum.inr (l, s')
                  | some (some a, s') => Sum.inr (a :: l, s'))
              (l, WSeq.nil))),
    Computation.BisimO
      (fun (c1 c2 : Computation ℕ) ↦
        ∃ (l : List α) (s : WSeq α),
          c1 =
              Computation.corec
                (fun (x : ℕ × WSeq α) ↦
                  match (motive := ℕ × WSeq α → ℕ ⊕ ℕ × WSeq α) x with
                  | (n, s) =>
                    match (motive := Option (Seq1 (Option α)) → ℕ ⊕ ℕ × WSeq α) Seq.destruct s with
                    | none => Sum.inl n
                    | some (none, s') => Sum.inr (n, s')
                    | some (some val, s') => Sum.inr (n + 1, s'))
                (l.length, s) ∧
            c2 =
              Computation.map (α := List α) List.length
                (Computation.corec
                  (fun (x : List α × WSeq α) ↦
                    match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
                    | (l, s) =>
                      match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
                      | none => Sum.inl l.reverse
                      | some (none, s') => Sum.inr (l, s')
                      | some (some a, s') => Sum.inr (a :: l, s'))
                  (l, s)))
      (Computation.destruct
        (Computation.corec
          (fun (x : ℕ × WSeq α) ↦
            match (motive := ℕ × WSeq α → ℕ ⊕ ℕ × WSeq α) x with
            | (n, s) =>
              match (motive := Option (Seq1 (Option α)) → ℕ ⊕ ℕ × WSeq α) Seq.destruct s with
              | none => Sum.inl n
              | some (none, s') => Sum.inr (n, s')
              | some (some val, s') => Sum.inr (n + 1, s'))
          (l.length, WSeq.nil)))
      (Computation.map (α := List α) List.length
          (Computation.corec
            (fun (x : List α × WSeq α) ↦
              match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
              | (l, s) =>
                match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
                | none => Sum.inl l.reverse
                | some (none, s') => Sum.inr (l, s')
                | some (some a, s') => Sum.inr (a :: l, s'))
            (l, WSeq.nil))).destruct
cons :
  ∀ (a : α) (s : WSeq α)
    (h :
      s1 =
          Computation.corec
            (fun (x : ℕ × WSeq α) ↦
              match (motive := ℕ × WSeq α → ℕ ⊕ ℕ × WSeq α) x with
              | (n, s) =>
                match (motive := Option (Seq1 (Option α)) → ℕ ⊕ ℕ × WSeq α) Seq.destruct s with
                | none => Sum.inl n
                | some (none, s') => Sum.inr (n, s')
                | some (some val, s') => Sum.inr (n + 1, s'))
            (l.length, WSeq.cons a s) ∧
        s2 =
          Computation.map (α := List α) List.length
            (Computation.corec
              (fun (x : List α × WSeq α) ↦
                match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
                | (l, s) =>
                  match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
                  | none => Sum.inl l.reverse
                  | some (none, s') => Sum.inr (l, s')
                  | some (some a, s') => Sum.inr (a :: l, s'))
              (l, WSeq.cons a s))),
    Computation.BisimO
      (fun (c1 c2 : Computation ℕ) ↦
        ∃ (l : List α) (s : WSeq α),
          c1 =
              Computation.corec
                (fun (x : ℕ × WSeq α) ↦
                  match (motive := ℕ × WSeq α → ℕ ⊕ ℕ × WSeq α) x with
                  | (n, s) =>
                    match (motive := Option (Seq1 (Option α)) → ℕ ⊕ ℕ × WSeq α) Seq.destruct s with
                    | none => Sum.inl n
                    | some (none, s') => Sum.inr (n, s')
                    | some (some val, s') => Sum.inr (n + 1, s'))
                (l.length, s) ∧
            c2 =
              Computation.map (α := List α) List.length
                (Computation.corec
                  (fun (x : List α × WSeq α) ↦
                    match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
                    | (l, s) =>
                      match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
                      | none => Sum.inl l.reverse
                      | some (none, s') => Sum.inr (l, s')
                      | some (some a, s') => Sum.inr (a :: l, s'))
                  (l, s)))
      (Computation.destruct
        (Computation.corec
          (fun (x : ℕ × WSeq α) ↦
            match (motive := ℕ × WSeq α → ℕ ⊕ ℕ × WSeq α) x with
            | (n, s) =>
              match (motive := Option (Seq1 (Option α)) → ℕ ⊕ ℕ × WSeq α) Seq.destruct s with
              | none => Sum.inl n
              | some (none, s') => Sum.inr (n, s')
              | some (some val, s') => Sum.inr (n + 1, s'))
          (l.length, WSeq.cons a s)))
      (Computation.map (α := List α) List.length
          (Computation.corec
            (fun (x : List α × WSeq α) ↦
              match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
              | (l, s) =>
                match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
                | none => Sum.inl l.reverse
                | some (none, s') => Sum.inr (l, s')
                | some (some a, s') => Sum.inr (a :: l, s'))
            (l, WSeq.cons a s))).destruct
⊢ Computation.BisimO
    (fun (c1 c2 : Computation ℕ) ↦
      ∃ (l : List α) (s : WSeq α),
        c1 =
            Computation.corec
              (fun (x : ℕ × WSeq α) ↦
                match (motive := ℕ × WSeq α → ℕ ⊕ ℕ × WSeq α) x with
                | (n, s) =>
                  match (motive := Option (Seq1 (Option α)) → ℕ ⊕ ℕ × WSeq α) Seq.destruct s with
                  | none => Sum.inl n
                  | some (none, s') => Sum.inr (n, s')
                  | some (some val, s') => Sum.inr (n + 1, s'))
              (l.length, s) ∧
          c2 =
            Computation.map (α := List α) List.length
              (Computation.corec
                (fun (x : List α × WSeq α) ↦
                  match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
                  | (l, s) =>
                    match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
                    | none => Sum.inl l.reverse
                    | some (none, s') => Sum.inr (l, s')
                    | some (some a, s') => Sum.inr (a :: l, s'))
                (l, s)))
    (Computation.destruct
      (Computation.corec
        (fun (x : ℕ × WSeq α) ↦
          match (motive := ℕ × WSeq α → ℕ ⊕ ℕ × WSeq α) x with
          | (n, s) =>
            match (motive := Option (Seq1 (Option α)) → ℕ ⊕ ℕ × WSeq α) Seq.destruct s with
            | none => Sum.inl n
            | some (none, s') => Sum.inr (n, s')
            | some (some val, s') => Sum.inr (n + 1, s'))
        (l.length, s)))
    (Computation.map (α := List α) List.length
        (Computation.corec
          (fun (x : List α × WSeq α) ↦
            match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
            | (l, s) =>
              match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l, s))).destruct
have think : ∀ (s : WSeq α)
  (h :
    s1 =
        Computation.corec
          (fun (x : ℕ × WSeq α) ↦
            match (motive := ℕ × WSeq α → ℕ ⊕ ℕ × WSeq α) x with
            | (n, s) =>
              match (motive := Option (Seq1 (Option α)) → ℕ ⊕ ℕ × WSeq α) Seq.destruct s with
              | none => Sum.inl n
              | some (none, s') => Sum.inr (n, s')
              | some (some val, s') => Sum.inr (n + 1, s'))
          (l.length, s.think) ∧
      s2 =
        Computation.map (α := List α) List.length
          (Computation.corec
            (fun (x : List α × WSeq α) ↦
              match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
              | (l, s) =>
                match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
                | none => Sum.inl l.reverse
                | some (none, s') => Sum.inr (l, s')
                | some (some a, s') => Sum.inr (a :: l, s'))
            (l, s.think))),
  Computation.BisimO
    (fun (c1 c2 : Computation ℕ) ↦
      ∃ (l : List α) (s : WSeq α),
        c1 =
            Computation.corec
              (fun (x : ℕ × WSeq α) ↦
                match (motive := ℕ × WSeq α → ℕ ⊕ ℕ × WSeq α) x with
                | (n, s) =>
                  match (motive := Option (Seq1 (Option α)) → ℕ ⊕ ℕ × WSeq α) Seq.destruct s with
                  | none => Sum.inl n
                  | some (none, s') => Sum.inr (n, s')
                  | some (some val, s') => Sum.inr (n + 1, s'))
              (l.length, s) ∧
          c2 =
            Computation.map (α := List α) List.length
              (Computation.corec
                (fun (x : List α × WSeq α) ↦
                  match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
                  | (l, s) =>
                    match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
                    | none => Sum.inl l.reverse
                    | some (none, s') => Sum.inr (l, s')
                    | some (some a, s') => Sum.inr (a :: l, s'))
                (l, s)))
    (Computation.destruct
      (Computation.corec
        (fun (x : ℕ × WSeq α) ↦
          match (motive := ℕ × WSeq α → ℕ ⊕ ℕ × WSeq α) x with
          | (n, s) =>
            match (motive := Option (Seq1 (Option α)) → ℕ ⊕ ℕ × WSeq α) Seq.destruct s with
            | none => Sum.inl n
            | some (none, s') => Sum.inr (n, s')
            | some (some val, s') => Sum.inr (n + 1, s'))
        (l.length, s.think)))
    (Computation.map (α := List α) List.length
        (Computation.corec
          (fun (x : List α × WSeq α) ↦
            match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
            | (l, s) =>
              match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l, s.think))).destruct
Tactic: induction s using WSeq.recOn with
  | nil => simp [nil]
  | cons a s => simpa using ⟨a::l, s, by simp, by simp⟩
  | think s => simpa using ⟨l, s, by simp, by simp⟩
Cleared hypotheses: s, h