{P : Sort u} →
  {classical : Bool} →
    {p : Lean.Name} →
      {classical' : Bool} →
        {p' : Lean.Name} →
          Mathlib.Tactic.ITauto.Proof.em classical p = Mathlib.Tactic.ITauto.Proof.em classical' p' →
            (classical = classical' → p = p' → P) → P