---

Step * 1 1 of Lemma map-square-board-cell


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

---

Latex:

---

Latex:

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


By

---

Latex:
(RWO    "-3"  0  THEN  Auto)

---

Home Index