∀ (s₁ s₂ : Lean.Grind.AC.Seq),
  s₁.sharesVar s₂ =
    match s₁, s₂ with
    | Lean.Grind.AC.Seq.var x, Lean.Grind.AC.Seq.var y => x == y
    | Lean.Grind.AC.Seq.var x, Lean.Grind.AC.Seq.cons y s₂ => x == y || (Lean.Grind.AC.Seq.var x).sharesVar s₂
    | Lean.Grind.AC.Seq.cons x s₁, Lean.Grind.AC.Seq.var y => x == y || s₁.sharesVar (Lean.Grind.AC.Seq.var y)
    | Lean.Grind.AC.Seq.cons x s₁, Lean.Grind.AC.Seq.cons y s₂ =>
      if (x == y) = true then true
      else if x < y then s₁.sharesVar (Lean.Grind.AC.Seq.cons y s₂) else (Lean.Grind.AC.Seq.cons x s₁).sharesVar s₂