---

Step * 1 1 3 of Lemma select_listify_id


1. T : Type
2. n : ℕ
3. f : ℕn ⟶ T
4. j : {...n - 1}@i
5. 0 ≤ (j + 1)
6. i : {j + 1..n-}@i
⊢ i - j + 1 < ||listify(f;j + 1;n)||
BY
{ (InstLemma `listify_length` [⌜T⌝;⌜j + 1⌝;⌜n⌝;⌜f⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  n  :  \mBbbN{}
3.  f  :  \mBbbN{}n  {}\mrightarrow{}  T
4.  j  :  \{...n  -  1\}@i
5.  0  \mleq{}  (j  +  1)
6.  i  :  \{j  +  1..n\msupminus{}\}@i
\mvdash{}  i  -  j  +  1  <  ||listify(f;j  +  1;n)||


By

---

Latex:
(InstLemma  `listify\_length`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}j  +  1\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index