---

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


1. T : Type
2. L : T List
3. f : T ⟶ partial(ℕ)
4. (Σ(f[L[i]] | i < ||L||))↓
5. x : T@i
6. i : ℕ
7. i < ||L||
8. x = L[i] ∈ T
9. ∀i:ℕ||L||. (f[L[i]])↓
10. (f[L[i]])↓
⊢ (f[x])↓
BY
{ TACTIC:(RevHypSubst (-3) (-1)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  L  :  T  List
3.  f  :  T  {}\mrightarrow{}  partial(\mBbbN{})
4.  (\mSigma{}(f[L[i]]  |  i  <  ||L||))\mdownarrow{}
5.  x  :  T@i
6.  i  :  \mBbbN{}
7.  i  <  ||L||
8.  x  =  L[i]
9.  \mforall{}i:\mBbbN{}||L||.  (f[L[i]])\mdownarrow{}
10.  (f[L[i]])\mdownarrow{}
\mvdash{}  (f[x])\mdownarrow{}


By

---

Latex:
TACTIC:(RevHypSubst  (-3)  (-1)\mcdot{}  THEN  Auto)

---

Home Index