{P : Sort u} →
  {info : Lean.InductiveVal} →
    {ctors : Array Lean.ConstructorVal} →
      {info' : Lean.InductiveVal} →
        {ctors' : Array Lean.ConstructorVal} →
          Lean.Elab.Tactic.BVDecide.Frontend.Normalize.MatchKind.enumWithDefault info ctors =
              Lean.Elab.Tactic.BVDecide.Frontend.Normalize.MatchKind.enumWithDefault info' ctors' →
            (info = info' → ctors = ctors' → P) → P