∀ (K : Type u) [inst : CommRing K] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p] (x : ℕ × K),
  (frobenius (PerfectClosure K p) p) (PerfectClosure.mk K p x) = PerfectClosure.mk K p (x.1, x.2 ^ p)