---

Step * of Lemma intlex-by-length

∀[l1,l2:ℤ List].  ↑l1 ≤_lex l2 supposing ||l1|| < ||l2||
BY
{ ((Auto THEN Unfold `intlex` 0)
   THEN RepeatFor 2 ((CallByValueReduce (0) THENA Auto))
   THEN AutoBoolCase ⌜||l1|| <z ||l2||⌝⋅) }

---

Latex:

---

Latex:
\mforall{}[l1,l2:\mBbbZ{}  List].    \muparrow{}l1  \mleq{}\_lex  l2  supposing  ||l1||  <  ||l2||


By

---

Latex:
((Auto  THEN  Unfold  `intlex`  0)
  THEN  RepeatFor  2  ((CallByValueReduce  (0)  THENA  Auto))
  THEN  AutoBoolCase  \mkleeneopen{}||l1||  <z  ||l2||\mkleeneclose{}\mcdot{})

---

Home Index