---

Step * 1 of Lemma intlex-aux_wf


1. ∀[n:ℕ]. ∀[l1,l2:{as:ℤ List| ||as|| = n ∈ ℤ} ].  (intlex-aux(l1;l2) ∈ 𝔹)
⊢ ∀[l1:ℤ List]. ∀[l2:{as:ℤ List| ||as|| = ||l1|| ∈ ℤ} ].  (intlex-aux(l1;l2) ∈ 𝔹)
BY
{ Auto }

---

Latex:

---

Latex:

1.  \mforall{}[n:\mBbbN{}].  \mforall{}[l1,l2:\{as:\mBbbZ{}  List|  ||as||  =  n\}  ].    (intlex-aux(l1;l2)  \mmember{}  \mBbbB{})
\mvdash{}  \mforall{}[l1:\mBbbZ{}  List].  \mforall{}[l2:\{as:\mBbbZ{}  List|  ||as||  =  ||l1||\}  ].    (intlex-aux(l1;l2)  \mmember{}  \mBbbB{})


By

---

Latex:
Auto

---

Home Index