---

Step * of Lemma intlex-aux-reflexive

∀[l1,l2:ℤ List].  intlex-aux(l1;l2) = tt supposing l1 = l2 ∈ (ℤ List)
BY
{ ((Assert ∀[l:ℤ List]. intlex-aux(l;l) = tt BY
          (InductionOnList THEN RecUnfold `intlex-aux` 0 THEN Reduce 0 THEN Auto))
   THEN Auto
   ) }

---

Latex:

---

Latex:
\mforall{}[l1,l2:\mBbbZ{}  List].    intlex-aux(l1;l2)  =  tt  supposing  l1  =  l2


By

---

Latex:
((Assert  \mforall{}[l:\mBbbZ{}  List].  intlex-aux(l;l)  =  tt  BY
                (InductionOnList  THEN  RecUnfold  `intlex-aux`  0  THEN  Reduce  0  THEN  Auto))
  THEN  Auto
  )

---

Home Index