---

Step * 1 1 1 of Lemma pi-rank-choices_wf


1. u : pi_prefix() × pi_term()
2. v : (pi_prefix() × pi_term()) List
3. ¬(0 = (||v|| + 1) ∈ ℤ)
⊢ (∃b∈[u / v]. 0 ≤ pi-rank(snd(b)))
BY
{ ((BLemma `l_exists_cons` THENM OrLeft) THEN Auto) }

---

Latex:

---

Latex:

1.  u  :  pi\_prefix()  \mtimes{}  pi\_term()
2.  v  :  (pi\_prefix()  \mtimes{}  pi\_term())  List
3.  \mneg{}(0  =  (||v||  +  1))
\mvdash{}  (\mexists{}b\mmember{}[u  /  v].  0  \mleq{}  pi-rank(snd(b)))


By

---

Latex:
((BLemma  `l\_exists\_cons`  THENM  OrLeft)  THEN  Auto)

---

Home Index