-- Module: Mathlib.Data.Seq.Basic
Goal:
α : Type u
s_1 s : Seq α
H :
  match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop)
    match (motive := Option (α × Seq α × Seq α) → Option (α × Seq α))
      match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) destruct nil with
      | none => none
      | some (a, b) => some (a, nil, b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          corec
            (fun (x : Seq α × Seq α) ↦
              match (motive := Option (Seq1 α) → Option (α × Seq α × Seq α)) x.1.destruct with
              | none =>
                match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) x.2.destruct with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.2))
            b),
    destruct nil with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_2 : Seq α),
        s =
            corec
              (fun (x : Seq α × Seq α) ↦
                match (motive := Option (Seq1 α) → Option (α × Seq α × Seq α)) x.1.destruct with
                | none =>
                  match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) x.2.destruct with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.2))
              (nil, s_2) ∧
          s' = s_2
  | x, x_1 => False
H₁ :
  ∀ (x : α) (s : Seq α),
    match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop)
      match (motive := Option (α × Seq α × Seq α) → Option (α × Seq α))
        match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) (cons x s).destruct with
        | none => none
        | some (a, b) => some (a, nil, b) with
      | none => none
      | some (a, b) =>
        some
          (a,
            corec
              (fun (x : Seq α × Seq α) ↦
                match (motive := Option (Seq1 α) → Option (α × Seq α × Seq α)) x.1.destruct with
                | none =>
                  match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) x.2.destruct with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.2))
              b),
      (cons x s).destruct with
    | none, none => True
    | some (a, s), some (a', s') =>
      a = a' ∧
        ∃ (s_2 : Seq α),
          s =
              corec
                (fun (x : Seq α × Seq α) ↦
                  match (motive := Option (Seq1 α) → Option (α × Seq α × Seq α)) x.1.destruct with
                  | none =>
                    match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) x.2.destruct with
                    | none => none
                    | some (a, b) => some (a, nil, b)
                  | some (a, s₁') => some (a, s₁', x.2))
                (nil, s_2) ∧
            s' = s_2
    | x, x_1 => False
⊢ match (motive := Option (Seq1 α) → Option (Seq1 α) → Prop)
    match (motive := Option (α × Seq α × Seq α) → Option (α × Seq α))
      match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) s.destruct with
      | none => none
      | some (a, b) => some (a, nil, b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          corec
            (fun (x : Seq α × Seq α) ↦
              match (motive := Option (Seq1 α) → Option (α × Seq α × Seq α)) x.1.destruct with
              | none =>
                match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) x.2.destruct with
                | none => none
                | some (a, b) => some (a, nil, b)
              | some (a, s₁') => some (a, s₁', x.2))
            b),
    s.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ (s_2 : Seq α),
        s =
            corec
              (fun (x : Seq α × Seq α) ↦
                match (motive := Option (Seq1 α) → Option (α × Seq α × Seq α)) x.1.destruct with
                | none =>
                  match (motive := Option (α × Seq α) → Option (α × Seq α × Seq α)) x.2.destruct with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.2))
              (nil, s_2) ∧
          s' = s_2
  | x, x_1 => False

Tactic:
cases s