∀ {K : Type u} [inst : CommRing K] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p] {L : Type u_1}
  (x x_1 : PerfectClosure K p),
  x = x_1 →
    ∀ (f f_1 : ℕ × K → L) (e_f : f = f_1) (hf : ∀ (x y : ℕ × K), PerfectClosure.R K p x y → f x = f y),
      x.liftOn f hf = x_1.liftOn f_1 ⋯