---

Step * 2 of Lemma sum-partial-list-has-value

.....wf..... 
1. T : Type
2. L : T List
3. f : T ⟶ partial(ℕ)
⊢ istype((Σ(f[L[i]] | i < ||L||))↓)
BY
{ (GenConclAtAddrType ⌜partial(ℕ)⌝ [1;1]⋅ THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  T  :  Type
2.  L  :  T  List
3.  f  :  T  {}\mrightarrow{}  partial(\mBbbN{})
\mvdash{}  istype((\mSigma{}(f[L[i]]  |  i  <  ||L||))\mdownarrow{})


By

---

Latex:
(GenConclAtAddrType  \mkleeneopen{}partial(\mBbbN{})\mkleeneclose{}  [1;1]\mcdot{}  THEN  Auto)

---

Home Index