---

Step * 1 1 of Lemma pa-sep-irrefl


1. p : {2...}
2. x1 : ℕ
3. x2 : p-adics(p)
⊢ ¬p-sep(x2;x2)
BY
{ Auto }

---

Latex:

---

Latex:

1.  p  :  \{2...\}
2.  x1  :  \mBbbN{}
3.  x2  :  p-adics(p)
\mvdash{}  \mneg{}p-sep(x2;x2)


By

---

Latex:
Auto

---

Home Index