---

Step * of Lemma ulist-ext

∀[T:Type]. ulist(T) ≡ T List
BY
{ (Auto THEN D 0) }

1
1. T : Type
⊢ ulist(T) ⊆r (T List)

2
1. T : Type
⊢ (T List) ⊆r ulist(T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  ulist(T)  \mequiv{}  T  List


By

---

Latex:
(Auto  THEN  D  0)

---

Home Index