---

Step * 2 1 of Lemma concat_map_upto


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'))
BY
{ (BLemma `iseg-map` THENA Auto) }

1
1. [T] : Type
2. f : ℕ ⟶ (T List)@i
3. t : ℕ@i
4. t' : ℕ@i
5. t < t'
⊢ upto(t + 1) ≤ 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{}  map(f;upto(t  +  1))  \mleq{}  map(f;upto(t'))


By

---

Latex:
(BLemma  `iseg-map`  THENA  Auto)

---

Home Index