---

Step * 1 1 of Lemma int-problem-dimension_wf


1. n : ℕ
2. {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
⊢ dim(inl <[], %3>) ∈ ℕ
BY
{ (D 2 THEN ProveWfLemma) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  \{L:\mBbbZ{}  List|  ||L||  =  (n  +  1)\}    List
\mvdash{}  dim(inl  <[],  \%3>)  \mmember{}  \mBbbN{}


By

---

Latex:
(D  2  THEN  ProveWfLemma)

---

Home Index