{P : Sort u} →
  {a : Lean.Name} →
    {a_1 : ℕ} →
      {a' : Lean.Name} →
        {a'_1 : ℕ} →
          Lean.Meta.LazyDiscrTree.Key.const a a_1 = Lean.Meta.LazyDiscrTree.Key.const a' a'_1 →
            (a = a' → a_1 = a'_1 → P) → P