---

Step * 2 2 of Lemma dataflow-valueall-type


1. A : 𝕌'
2. B : Type
3. ↓A
⊢ valueall-type(λ2P.A ⟶ (P × B)^1 Top)
BY
{ Unfold `so_lambda` 0 }

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

---

Latex:

---

Latex:

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


By

---

Latex:
Unfold  `so\_lambda`  0

---

Home Index