{P : Sort u} →
  {m n : Q(ℕ)} →
    {t : Tactic.NormNum.NotPowerCertificate m n} →
      {m' n' : Q(ℕ)} →
        {t' : Tactic.NormNum.NotPowerCertificate m' n'} →
          m = m' → n = n' → t ≍ t' → Tactic.NormNum.NotPowerCertificate.noConfusionType P t t'