---

Step * of Lemma fan-implies-bar-sep

∀[T:Type]. (Fan_d(T) ⇒ (∃size:ℕ. T ~ ℕsize) ⇒ BarSep(T;T))
BY
{ (Auto THEN D 0 THEN Auto THEN ExRepD THEN CaseNat 0 `size') }

1
1. [T] : Type
2. Fan_d(T)
3. size : ℕ
4. T ~ ℕsize
5. A : (T List) ⟶ ℙ
6. B : (T List) ⟶ ℙ
7. Decidable(A)
8. Decidable(B)
9. jbar(T;T;A;B)
10. size = 0 ∈ ℤ
⊢ tbar(T;A) ∨ tbar(T;B)

2
1. [T] : Type
2. Fan_d(T)
3. size : ℕ
4. T ~ ℕsize
5. A : (T List) ⟶ ℙ
6. B : (T List) ⟶ ℙ
7. Decidable(A)
8. Decidable(B)
9. jbar(T;T;A;B)
10. ¬(size = 0 ∈ ℤ)
⊢ tbar(T;A) ∨ tbar(T;B)

---

Latex:

---

Latex:
\mforall{}[T:Type].  (Fan\_d(T)  {}\mRightarrow{}  (\mexists{}size:\mBbbN{}.  T  \msim{}  \mBbbN{}size)  {}\mRightarrow{}  BarSep(T;T))


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto  THEN  ExRepD  THEN  CaseNat  0  `size')

---

Home Index