{n : Q(ℕ)} →
  {P : Sort u} →
    {n' : Q(ℕ)} →
      {pf : «$n» =Q «$n'».succ} →
        {n'' : Q(ℕ)} →
          {pf' : «$n» =Q «$n''».succ} →
            Mathlib.Meta.Nat.UnifyZeroOrSuccResult.succ n' pf = Mathlib.Meta.Nat.UnifyZeroOrSuccResult.succ n'' pf' →
              (n' = n'' → P) → P