∀ (K : Type u_1) [inst : CommRing K] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p] (n : ℕ) (x : K),
  PerfectClosure.R K p ((n, x).1, -(n, x).2) ((n + 1, (frobenius K p) x).1, -(n + 1, (frobenius K p) x).2)