∀ (motive : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Sort u_1) (α : Sort u✝) (β : α → Sort v✝) (f : (x : α) → β x)
  (rel : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → α → Prop) (s₂ s₁ : Lean.Grind.AC.Seq)
  (h_1 :
    (x y : Lean.Grind.AC.Var) →
      ((y_1 : α) → rel (Lean.Grind.AC.Seq.var x) (Lean.Grind.AC.Seq.var y) y_1 → β y_1) →
        motive (Lean.Grind.AC.Seq.var x) (Lean.Grind.AC.Seq.var y))
  (h_2 :
    (x y : Lean.Grind.AC.Var) →
      (s : Lean.Grind.AC.Seq) →
        ((y_1 : α) → rel (Lean.Grind.AC.Seq.var x) (Lean.Grind.AC.Seq.cons y s) y_1 → β y_1) →
          motive (Lean.Grind.AC.Seq.var x) (Lean.Grind.AC.Seq.cons y s))
  (h_3 :
    (x : Lean.Grind.AC.Var) →
      (s : Lean.Grind.AC.Seq) →
        (x_1 : Lean.Grind.AC.Var) →
          ((y : α) → rel (Lean.Grind.AC.Seq.cons x s) (Lean.Grind.AC.Seq.var x_1) y → β y) →
            motive (Lean.Grind.AC.Seq.cons x s) (Lean.Grind.AC.Seq.var x_1))
  (h_4 :
    (x : Lean.Grind.AC.Var) →
      (s₂ : Lean.Grind.AC.Seq) →
        (y : Lean.Grind.AC.Var) →
          (s₁ : Lean.Grind.AC.Seq) →
            ((y_1 : α) → rel (Lean.Grind.AC.Seq.cons x s₂) (Lean.Grind.AC.Seq.cons y s₁) y_1 → β y_1) →
              motive (Lean.Grind.AC.Seq.cons x s₂) (Lean.Grind.AC.Seq.cons y s₁)),
  ((match (motive := (s₂ s₁ : Lean.Grind.AC.Seq) → ((y : α) → rel s₂ s₁ y → β y) → motive s₂ s₁) s₂, s₁ with
      | Lean.Grind.AC.Seq.var x, Lean.Grind.AC.Seq.var y => fun x_1 => h_1 x y x_1
      | Lean.Grind.AC.Seq.var x, Lean.Grind.AC.Seq.cons y s => fun x_1 => h_2 x y s x_1
      | Lean.Grind.AC.Seq.cons x s, Lean.Grind.AC.Seq.var x_1 => fun x_2 => h_3 x s x_1 x_2
      | Lean.Grind.AC.Seq.cons x s₂, Lean.Grind.AC.Seq.cons y s₁ => fun x_1 => h_4 x s₂ y s₁ x_1)
      fun y h => f y) =
    match s₂, s₁ with
    | Lean.Grind.AC.Seq.var x, Lean.Grind.AC.Seq.var y => h_1 x y fun y_1 h => f y_1
    | Lean.Grind.AC.Seq.var x, Lean.Grind.AC.Seq.cons y s => h_2 x y s fun y_1 h => f y_1
    | Lean.Grind.AC.Seq.cons x s, Lean.Grind.AC.Seq.var x_1 => h_3 x s x_1 fun y h => f y
    | Lean.Grind.AC.Seq.cons x s₂, Lean.Grind.AC.Seq.cons y s₁ => h_4 x s₂ y s₁ fun y_1 h => f y_1