---

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

∀[T:Type]. ∀[L:T List]. ∀[f:T ⟶ partial(ℕ)].  ∀x:T. (f[x])↓ supposing (x ∈ L) supposing (Σ(f[L[i]] | i < ||L||))↓
BY
{ TACTIC:(RepeatFor 3 (Intro) THEN At ⌜Type⌝ (D 0)⋅) }

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

2
.....wf..... 
1. T : Type
2. L : T List
3. f : T ⟶ partial(ℕ)
⊢ istype((Σ(f[L[i]] | i < ||L||))↓)

---

Latex:

---

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


By

---

Latex:
TACTIC:(RepeatFor  3  (Intro)  THEN  At  \mkleeneopen{}Type\mkleeneclose{}  (D  0)\mcdot{})

---

Home Index