---

Step * of Lemma fan-bar-sep

∀[T:Type]. (Fan(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(T)
3. size : ℕ
4. T ~ ℕsize
5. A : n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹
6. B : n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹
7. jbar(A;B)
8. size = 0 ∈ ℤ
⊢ bar(A) ∨ bar(B)

2
1. [T] : Type
2. Fan(T)
3. size : ℕ
4. T ~ ℕsize
5. A : n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹
6. B : n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹
7. jbar(A;B)
8. ¬(size = 0 ∈ ℤ)
⊢ bar(A) ∨ bar(B)

---

Latex:

---

Latex:
\mforall{}[T:Type].  (Fan(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