---

Step * of Lemma rank-Ex1_wf

∀[T:Type]. ∀[t:RankEx1(T)].  (rank-Ex1(t) ∈ ℕ)
BY
{ ((UnivCD THENA Auto)
   THEN SimpleDatatypeInduction (-1)
   THEN RecUnfold `rank-Ex1` 0
   THEN Reduce 0
   THEN Try (CompleteAuto)) }

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

---

Latex:


\mforall{}[T:Type].  \mforall{}[t:RankEx1(T)].    (rank-Ex1(t)  \mmember{}  \mBbbN{})


By

((UnivCD  THENA  Auto)
  THEN  SimpleDatatypeInduction  (-1)
  THEN  RecUnfold  `rank-Ex1`  0
  THEN  Reduce  0
  THEN  Try  (CompleteAuto))

---

Home Index