---

Step * 1 of Lemma pa-sep-irrefl


1. p : {2...}
2. x1 : ℕ
3. x2 : p-adics(p)
4. p-sep(x2;x2)
⊢ False
BY
{ (MoveToConcl (-1) THEN Fold `not` 0) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
(MoveToConcl  (-1)  THEN  Fold  `not`  0)

---

Home Index