---

Step * 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||))↓
⊢ ∀x:T. (f[x])↓ supposing (x ∈ L)
BY
{ TACTIC:(UnivCD THENA Auto) }

1
1. T : Type
2. L : T List
3. f : T ⟶ partial(ℕ)
4. (Σ(f[L[i]] | i < ||L||))↓
5. x : T@i
6. (x ∈ L)
⊢ (f[x])↓

---

Latex:

---

Latex:

1.  T  :  Type
2.  L  :  T  List
3.  f  :  T  {}\mrightarrow{}  partial(\mBbbN{})
4.  (\mSigma{}(f[L[i]]  |  i  <  ||L||))\mdownarrow{}
\mvdash{}  \mforall{}x:T.  (f[x])\mdownarrow{}  supposing  (x  \mmember{}  L)


By

---

Latex:
TACTIC:(UnivCD  THENA  Auto)

---

Home Index