---

Step * of Lemma islist-iff-length-has-value

No Annotations
∀[T:Type]. ∀[t:colist(T)].  uiff((is-list(t))↓;(||t||)↓)
BY
{ (Intros THEN RepeatFor 2 (At ⌜Type⌝ (D 0)⋅)) }

1
1. T : Type
2. t : colist(T)
3. (is-list(t))↓
⊢ (||t||)↓

2
.....wf..... 
1. T : Type
2. t : colist(T)
⊢ istype((is-list(t))↓)

3
1. T : Type
2. t : colist(T)
3. (||t||)↓
⊢ (is-list(t))↓

4
.....wf..... 
1. T : Type
2. t : colist(T)
⊢ istype((||t||)↓)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[t:colist(T)].    uiff((is-list(t))\mdownarrow{};(||t||)\mdownarrow{})


By

---

Latex:
(Intros  THEN  RepeatFor  2  (At  \mkleeneopen{}Type\mkleeneclose{}  (D  0)\mcdot{}))

---

Home Index