∀ {info : Lean.InductiveVal} {ctors : Array Lean.ConstructorVal} {info_1 : Lean.InductiveVal}
  {ctors_1 : Array Lean.ConstructorVal},
  Lean.Elab.Tactic.BVDecide.Frontend.Normalize.MatchKind.enumWithDefault info ctors =
      Lean.Elab.Tactic.BVDecide.Frontend.Normalize.MatchKind.enumWithDefault info_1 ctors_1 →
    info = info_1 ∧ ctors = ctors_1