∀ (x : Lean.Name) (p : Mathlib.Tactic.ITauto.Proof) (x_1 : Lean.Name) (p_1 : Mathlib.Tactic.ITauto.Proof),
  (Mathlib.Tactic.ITauto.Proof.intro x p = Mathlib.Tactic.ITauto.Proof.intro x_1 p_1) = (x = x_1 ∧ p = p_1)