(motive : Lean.Name → Lean.Name → Sort u_1) →
  (n₁ n₂ : Lean.Name) →
    (Unit → motive Lean.Name.anonymous Lean.Name.anonymous) →
      ((x : Lean.Name) → motive Lean.Name.anonymous x) →
        ((x : Lean.Name) → motive x Lean.Name.anonymous) →
          ((p₁ : Lean.Name) → (i₁ : ℕ) → (p₂ : Lean.Name) → (i₂ : ℕ) → motive (p₁.num i₁) (p₂.num i₂)) →
            ((pre : Lean.Name) → (i : ℕ) → (pre_1 : Lean.Name) → (str : String) → motive (pre.num i) (pre_1.str str)) →
              ((pre : Lean.Name) →
                  (str : String) → (pre_1 : Lean.Name) → (i : ℕ) → motive (pre.str str) (pre_1.num i)) →
                ((p₁ : Lean.Name) → (n₁ : String) → (p₂ : Lean.Name) → (n₂ : String) → motive (p₁.str n₁) (p₂.str n₂)) →
                  motive n₁ n₂