---

Step * 2 of Lemma dataflow-valueall-type


1. A : 𝕌'
2. B : Type
3. ↓A
⊢ ∃n:ℕ. valueall-type(λ2P.A ─→ (P × B)^n Top)
BY
{ At ⌈𝕌'⌉ (With ⌈1⌉ (D 0))⋅ }

1
.....wf..... 
1. A : 𝕌'
2. B : Type
3. ↓A
⊢ 1 ∈ ℕ

2
1. A : 𝕌'
2. B : Type
3. ↓A
⊢ valueall-type(λ2P.A ─→ (P × B)^1 Top)

3
.....wf..... 
1. A : 𝕌'
2. B : Type
3. ↓A
4. n : ℕ
⊢ valueall-type(λ2P.A ─→ (P × B)^n Top) ∈ 𝕌'

---

Latex:

---

Latex:

1.  A  :  \mBbbU{}'
2.  B  :  Type
3.  \mdownarrow{}A
\mvdash{}  \mexists{}n:\mBbbN{}.  valueall-type(\mlambda{}\msubtwo{}P.A  {}\mrightarrow{}  (P  \mtimes{}  B)\^{}n  Top)


By

---

Latex:
At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}  (With  \mkleeneopen{}1\mkleeneclose{}  (D  0))\mcdot{}

---

Home Index