---

Step * 2 2 1 of Lemma dataflow-valueall-type


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

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

---

Latex:

---

Latex:

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


By

---

Latex:
(Unfold  `fun\_exp`  0  THEN  Reduce  0)

---

Home Index