---

Step * 1 1 1 of Lemma initseg_sum0


1. h : @i
2. t :  List@i
 l_sum([h / firstn(0;t)]) = h
BY
{ (InstLemma `first0` [t] THENA Auto) }

1
1. h : @i
2. t :  List@i
3. firstn(0;t) ~ []
 l_sum([h / firstn(0;t)]) = h

---

Latex:



1.  h  :  \mBbbZ{}@i
2.  t  :  \mBbbZ{}  List@i
\mvdash{}  l\_sum([h  /  firstn(0;t)])  =  h


By

(InstLemma  `first0`  [\mkleeneopen{}t\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index