---

Step * of Lemma finite-union

∀S,T:Type.  (finite(S) ∧ finite(T) ⇐⇒ finite(S + T))
BY
{ (Auto THEN All (Unfold `finite`)⋅ THEN ExRepD) }

1
1. S : Type
2. T : Type
3. n1 : ℕ
4. S ~ ℕn1
5. n : ℕ
6. T ~ ℕn
⊢ ∃n:ℕ. S + T ~ ℕn

2
1. S : Type
2. T : Type
3. n : ℕ
4. S + T ~ ℕn
⊢ ∃n:ℕ. S ~ ℕn

3
1. S : Type
2. T : Type
3. n : ℕ
4. S + T ~ ℕn
⊢ ∃n:ℕ. T ~ ℕn

---

Latex:

---

Latex:
\mforall{}S,T:Type.    (finite(S)  \mwedge{}  finite(T)  \mLeftarrow{}{}\mRightarrow{}  finite(S  +  T))


By

---

Latex:
(Auto  THEN  All  (Unfold  `finite`)\mcdot{}  THEN  ExRepD)

---

Home Index