---

Step * 1 1 1 of Lemma intlex-antisym


1. l1 : ℤ List
2. l2 : ℤ List
3. ||l2|| < ||l1||
4. ||l1|| < ||l2||
⊢ tt = tt ⇒ tt = tt ⇒ (l1 = l2 ∈ (ℤ List))
BY
{ Auto }

---

Latex:

---

Latex:

1.  l1  :  \mBbbZ{}  List
2.  l2  :  \mBbbZ{}  List
3.  ||l2||  <  ||l1||
4.  ||l1||  <  ||l2||
\mvdash{}  tt  =  tt  {}\mRightarrow{}  tt  =  tt  {}\mRightarrow{}  (l1  =  l2)


By

---

Latex:
Auto

---

Home Index