---

Step * 1 1 of Lemma concat_map_upto


1. T : Type
2. f : ℕ ⟶ (T List)@i
3. t : ℕ@i
4. t' : ℕ@i
5. t < t'
⊢ f t ~ concat([f t])
BY
{ ((RWO "concat-cons" 0 THENA Auto) THEN Reduce 0 THEN RWO "append_nil_sq" 0 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{}  f  t  \msim{}  concat([f  t])


By

---

Latex:
((RWO  "concat-cons"  0  THENA  Auto)  THEN  Reduce  0  THEN  RWO  "append\_nil\_sq"  0  THEN  Auto)

---

Home Index