∀ (x x_1 : Lean.Grind.AC.Seq),
  Lean.Grind.AC.instBEqSeq.beq x x_1 =
    match x, x_1 with
    | Lean.Grind.AC.Seq.var a, Lean.Grind.AC.Seq.var b => a == b
    | Lean.Grind.AC.Seq.cons a a_1, Lean.Grind.AC.Seq.cons b b_1 => a == b && Lean.Grind.AC.instBEqSeq.beq a_1 b_1
    | x, x_2 => false