---

Step * 2 1 1 1 of Lemma intlex-cons


1. l1 : ℤ List
2. l2 : ℤ List
3. x : ℤ
4. y : ℤ
5. x ≠ y
6. ¬x < y
7. ¬||l1|| < ||l2||
8. ||l1|| = ||l2|| ∈ ℤ
9. ↑(inr Ax )
⊢ x = y ∈ ℤ
BY
{ (RepUR ``assert`` -1 THEN Auto) }

---

Latex:

---

Latex:

1.  l1  :  \mBbbZ{}  List
2.  l2  :  \mBbbZ{}  List
3.  x  :  \mBbbZ{}
4.  y  :  \mBbbZ{}
5.  x  \mneq{}  y
6.  \mneg{}x  <  y
7.  \mneg{}||l1||  <  ||l2||
8.  ||l1||  =  ||l2||
9.  \muparrow{}(inr  Ax  )
\mvdash{}  x  =  y


By

---

Latex:
(RepUR  ``assert``  -1  THEN  Auto)

---

Home Index