---

Step * 1 1 1 of Lemma rank-Ex1_wf


1. T : Type
2. t1 : RankEx1(T) List
3. ∀i:ℕ||t1||. (rank-Ex1(t1[i]) ∈ ℕ)
⊢ map(λu.rank-Ex1(u);t1) ∈ ℕ List
BY
{ (RWO "map-as-map-upto" 0 THEN Auto) }

---

Latex:



1.  T  :  Type
2.  t1  :  RankEx1(T)  List
3.  \mforall{}i:\mBbbN{}||t1||.  (rank-Ex1(t1[i])  \mmember{}  \mBbbN{})
\mvdash{}  map(\mlambda{}u.rank-Ex1(u);t1)  \mmember{}  \mBbbN{}  List


By

(RWO  "map-as-map-upto"  0  THEN  Auto)

---

Home Index