---

Step * 1 of Lemma board-cell_wf


1. T : Type
2. n : ℕ
3. b : T List List
4. ||b|| = n ∈ ℤ
5. ∀i:ℕn. (||b[i]|| = n ∈ ℤ)
6. i : ℕn
7. j : ℕn
⊢ j < ||b[i]||
BY
{ (RWO "5" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  n  :  \mBbbN{}
3.  b  :  T  List  List
4.  ||b||  =  n
5.  \mforall{}i:\mBbbN{}n.  (||b[i]||  =  n)
6.  i  :  \mBbbN{}n
7.  j  :  \mBbbN{}n
\mvdash{}  j  <  ||b[i]||


By

---

Latex:
(RWO  "5"  0  THEN  Auto)

---

Home Index