(a b m c₀ : Q(ℕ)) →
  (motive :
      (c : Q(ℕ)) × Q(Mathlib.Meta.NormNum.IsNatPowModT ((«$a».pow 1).mod «$m» = «$c₀») «$a» «$b» «$m» «$c») →
        Sort u_1) →
    (x : (c : Q(ℕ)) × Q(Mathlib.Meta.NormNum.IsNatPowModT ((«$a».pow 1).mod «$m» = «$c₀») «$a» «$b» «$m» «$c»)) →
      ((c : Q(ℕ)) →
          (p : Q(Mathlib.Meta.NormNum.IsNatPowModT ((«$a».pow 1).mod «$m» = «$c₀») «$a» «$b» «$m» «$c»)) →
            motive ⟨c, p⟩) →
        motive x