{p : ℕ} →
  [inst : Fact (Nat.Prime p)] →
    {R : Type u₁} →
      [inst_1 : CommSemiring R] →
        [inst_2 : CharP R p] →
          {P : Type u₂} →
            [inst_3 : CommSemiring P] →
              [inst_4 : CharP P p] →
                [inst_5 : PerfectRing P p] →
                  {π : P →+* R} →
                    {motive : PerfectionMap p π → Sort u} →
                      ((injective :
                            ∀ ⦃x y : P⦄,
                              (∀ (n : ℕ),
                                  π ((⇑(frobeniusEquiv P p).symm)^[n] x) = π ((⇑(frobeniusEquiv P p).symm)^[n] y)) →
                                x = y) →
                          (surjective :
                              ∀ (f : ℕ → R),
                                (∀ (n : ℕ), f (n + 1) ^ p = f n) →
                                  ∃ x, ∀ (n : ℕ), π ((⇑(frobeniusEquiv P p).symm)^[n] x) = f n) →
                            motive ⋯) →
                        (t : PerfectionMap p π) → motive t