---

Step * 1 of Lemma equipollent-nsub


1. n : ℕ
2. m : ℕ
3. n = m ∈ ℤ
⊢ ℕn ~ ℕm
BY
{ xxx(HypSubst' -1 0 THEN RelRST THEN Auto)xxx }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  m  :  \mBbbN{}
3.  n  =  m
\mvdash{}  \mBbbN{}n  \msim{}  \mBbbN{}m


By

---

Latex:
xxx(HypSubst'  -1  0  THEN  RelRST  THEN  Auto)xxx

---

Home Index