∀ (x x_1 : Lean.Name),
  (x = Lean.Name.anonymous → x_1 = Lean.Name.anonymous → False) →
    (∀ (p₁ : Lean.Name) (s₁ : String) (p₂ : Lean.Name) (s₂ : String), x = p₁.str s₁ → x_1 = p₂.str s₂ → False) →
      (∀ (p₁ : Lean.Name) (n₁ : ℕ) (p₂ : Lean.Name) (n₂ : ℕ), x = p₁.num n₁ → x_1 = p₂.num n₂ → False) →
        x.beq x_1 = false