---

Step * 2 of Lemma concat_map_upto


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

1
1. [T] : Type
2. f : ℕ ⟶ (T List)@i
3. t : ℕ@i
4. t' : ℕ@i
5. t < t'
⊢ map(f;upto(t + 1)) ≤ map(f;upto(t'))

---

Latex:

---

Latex:

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


By

---

Latex:
(BLemma  `concat\_iseg`  THENA  Auto)

---

Home Index