---

Step * 1 1 of Lemma rank-Ex1_wf

.....wf..... 
1. T : Type
2. t1 : RankEx1(T) List
3. ∀i:ℕ||t1||. (rank-Ex1(t1[i]) ∈ ℕ)
⊢ map(λu.rank-Ex1(u);t1) ∈ ℤ List
BY
{ SubsumeC ⌈ℕ List⌉⋅ }

1
1. T : Type
2. t1 : RankEx1(T) List
3. ∀i:ℕ||t1||. (rank-Ex1(t1[i]) ∈ ℕ)
⊢ map(λu.rank-Ex1(u);t1) ∈ ℕ List

2
1. T : Type
2. t1 : RankEx1(T) List
3. ∀i:ℕ||t1||. (rank-Ex1(t1[i]) ∈ ℕ)
4. map(λu.rank-Ex1(u);t1) = map(λu.rank-Ex1(u);t1) ∈ (ℕ List)
⊢ (ℕ List) ⊆r (ℤ List)

---

Latex:


.....wf..... 
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{}  \mBbbZ{}  List


By

SubsumeC  \mkleeneopen{}\mBbbN{}  List\mkleeneclose{}\mcdot{}

---

Home Index