---

Step * of Lemma imax-list-member

∀L:ℤ List. (imax-list(L) ∈ L) supposing 0 < ||L||
BY
{ (RepUR ``imax-list`` 0
   THEN Auto
   THEN BLemma `combine-list-member`⋅
   THEN Auto
   THEN (RWO "imax_unfold" 0 THENA Auto)
   THEN AutoSplit
   THEN TrivialOr) }

---

Latex:

---

Latex:
\mforall{}L:\mBbbZ{}  List.  (imax-list(L)  \mmember{}  L)  supposing  0  <  ||L||


By

---

Latex:
(RepUR  ``imax-list``  0
  THEN  Auto
  THEN  BLemma  `combine-list-member`\mcdot{}
  THEN  Auto
  THEN  (RWO  "imax\_unfold"  0  THENA  Auto)
  THEN  AutoSplit
  THEN  TrivialOr)

---

Home Index