∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommRing R] {I : Ideal R} [inst_2 : CharP (R ⧸ I) p]
  (x x_1 : Perfection (R ⧸ I) p), x = x_1 → ∀ (a a_1 : ℕ), a = a_1 → x.teichmullerAux a = x_1.teichmullerAux a_1