---

Step * 1 1 2 of Lemma rank-Ex1_wf


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)
BY
{ Auto }

---

Latex:



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


By

Auto

---

Home Index