---

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


1. A : 𝕌'
2. B : Type
3. ↓A
4. n : ℕ
⊢ valueall-type(λP.(A ─→ (P × B))^n Top) ∈ 𝕌'
BY
{ ((InstLemma `valueall-type_wf` [⌈parm{i'}⌉]⋅ THENA Auto) THEN BHyp -1 ) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
((InstLemma  `valueall-type\_wf`  [\mkleeneopen{}parm\{i'\}\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  BHyp  -1  )

---

Home Index