---

Step * 2 1 1 of Lemma concat_map_upto


1. [T] : Type
2. f : ℕ ⟶ (T List)@i
3. t : ℕ@i
4. t' : ℕ@i
5. t < t'
⊢ upto(t + 1) ≤ upto(t')
BY
{ (BLemma `upto_iseg` THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  f  :  \mBbbN{}  {}\mrightarrow{}  (T  List)@i
3.  t  :  \mBbbN{}@i
4.  t'  :  \mBbbN{}@i
5.  t  <  t'
\mvdash{}  upto(t  +  1)  \mleq{}  upto(t')


By

---

Latex:
(BLemma  `upto\_iseg`  THEN  Auto)\mcdot{}

---

Home Index