---

Step * 1 of Lemma concat_map_upto

.....equality..... 
1. T : Type
2. f : ℕ ⟶ (T List)@i
3. t : ℕ@i
4. t' : ℕ@i
5. t < t'
⊢ concat(map(f;upto(t))) @ (f t) ~ concat(map(f;upto(t + 1)))
BY
{ ((RWW "upto_add_1 map_append_sq concat_append" 0 THENM Reduce 0 THENM EqCD THEN Try (Trivial)) THENA Auto) }

1
1. T : Type
2. f : ℕ ⟶ (T List)@i
3. t : ℕ@i
4. t' : ℕ@i
5. t < t'
⊢ f t ~ concat([f t])

---

Latex:

---

Latex:
.....equality..... 
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)))  @  (f  t)  \msim{}  concat(map(f;upto(t  +  1)))


By

---

Latex:
((RWW  "upto\_add\_1  map\_append\_sq  concat\_append"  0  THENM  Reduce  0  THENM  EqCD  THEN  Try  (Trivial))
  THENA  Auto
  )

---

Home Index