---

Step * 1 1 1 1 of Lemma initseg_sum0


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

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

---

Latex:



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


By

(HypSubst  3  0  THENA  Auto)

---

Home Index