---

Step * of Lemma intlex-cons-same

∀[l1,l2:ℤ List]. ∀[x:ℤ].  uiff(↑[x / l1] ≤_lex [x / l2];↑l1 ≤_lex l2)
BY
{ ((UnivCD THENA Auto) THEN RWO "intlex-cons" 0 THEN Auto) }

1
1. l1 : ℤ List
2. l2 : ℤ List
3. x : ℤ
4. ||l1|| < ||l2|| ∨ (x < x ∧ (||l1|| = ||l2|| ∈ ℤ)) ∨ ((x = x ∈ ℤ) ∧ (↑l1 ≤_lex l2))
⊢ ↑l1 ≤_lex l2

---

Latex:

---

Latex:
\mforall{}[l1,l2:\mBbbZ{}  List].  \mforall{}[x:\mBbbZ{}].    uiff(\muparrow{}[x  /  l1]  \mleq{}\_lex  [x  /  l2];\muparrow{}l1  \mleq{}\_lex  l2)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RWO  "intlex-cons"  0  THEN  Auto)

---

Home Index