---

Step * 2 2 of Lemma hdataflow-valueall-type


1. A : Type
2. B : Type
3. A
4. n : ℕ
⊢ λP.(A ─→ (P × bag(B))?)^n Top ∈ Type
BY
{ (GenConclAtAddrType ⌈Type ─→ Type⌉ [2;1]⋅ THEN Auto) }

---

Latex:



1.  A  :  Type
2.  B  :  Type
3.  A
4.  n  :  \mBbbN{}
\mvdash{}  \mlambda{}P.(A  {}\mrightarrow{}  (P  \mtimes{}  bag(B))?)\^{}n  Top  \mmember{}  Type


By

(GenConclAtAddrType  \mkleeneopen{}Type  {}\mrightarrow{}  Type\mkleeneclose{}  [2;1]\mcdot{}  THEN  Auto)

---

Home Index