---

Step * 1 1 of Lemma finite-union


1. S : Type
2. T : Type
3. n1 : ℕ
4. S ~ ℕn1
5. n : ℕ
6. T ~ ℕn
⊢ S + T ~ ℕn1 + ℕn
BY
{ (RWO "-3< -1<" 0 THEN Auto THEN RelRST THEN Auto) }

---

Latex:

---

Latex:

1.  S  :  Type
2.  T  :  Type
3.  n1  :  \mBbbN{}
4.  S  \msim{}  \mBbbN{}n1
5.  n  :  \mBbbN{}
6.  T  \msim{}  \mBbbN{}n
\mvdash{}  S  +  T  \msim{}  \mBbbN{}n1  +  \mBbbN{}n


By

---

Latex:
(RWO  "-3<  -1<"  0  THEN  Auto  THEN  RelRST  THEN  Auto)

---

Home Index