---

Step * 2 3 of Lemma dataflow-valueall-type

.....wf..... 
1. A : 𝕌'
2. B : Type
3. ↓A
4. n : ℕ
⊢ valueall-type(λ2P.A ─→ (P × B)^n Top) ∈ 𝕌'
BY
{ Unfold `so_lambda` 0⋅ }

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

---

Latex:

---

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


By

---

Latex:
Unfold  `so\_lambda`  0\mcdot{}

---

Home Index