∀ (x : Lean.Grind.AC.Var) (s_2 : Lean.Grind.AC.Seq),
  (Lean.Grind.AC.Seq.cons x s_2).eraseDup =
    match s_2.eraseDup with
    | Lean.Grind.AC.Seq.var y =>
      if Nat.beq x y = true then Lean.Grind.AC.Seq.var x else Lean.Grind.AC.Seq.cons x (Lean.Grind.AC.Seq.var y)
    | Lean.Grind.AC.Seq.cons y s' =>
      if Nat.beq x y = true then Lean.Grind.AC.Seq.cons y s' else Lean.Grind.AC.Seq.cons x (Lean.Grind.AC.Seq.cons y s')