---

Step * of Lemma board-cell_wf

∀[T:Type]. ∀[n:ℕ]. ∀[b:square-board(n;T)]. ∀[i,j:ℕn].  (board-cell(b;i;j) ∈ T)
BY
{ (Auto THEN D 3 THEN ProveWfLemma) }

1
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]||

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[b:square-board(n;T)].  \mforall{}[i,j:\mBbbN{}n].    (board-cell(b;i;j)  \mmember{}  T)


By

---

Latex:
(Auto  THEN  D  3  THEN  ProveWfLemma)

---

Home Index