---

Step * of Lemma ranked-eo-first

∀[L,rk:Top]. ∀[e:Id × ℤ].  (first(e) ~ (snd(e) =z 0))
BY
{ Auto }

1
1. L : Top
2. rk : Top
3. e : Id × ℤ
⊢ first(e) ~ (snd(e) =z 0)

---

Latex:

---

Latex:
\mforall{}[L,rk:Top].  \mforall{}[e:Id  \mtimes{}  \mBbbZ{}].    (first(e)  \msim{}  (snd(e)  =\msubz{}  0))


By

---

Latex:
Auto

---

Home Index