---

Step * 1 1 of Lemma is-list-if-has-value-decomp

.....wf..... 
1. t : ListLike
2. (t)↓
⊢ t ∈ Unit ⋃ (Top × ListLike)
BY
{ (InstLemma `is-list-if-has-value-ext` [] THEN D (-1) THEN BLemma `termination` THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  t  :  ListLike
2.  (t)\mdownarrow{}
\mvdash{}  t  \mmember{}  Unit  \mcup{}  (Top  \mtimes{}  ListLike)


By

---

Latex:
(InstLemma  `is-list-if-has-value-ext`  []  THEN  D  (-1)  THEN  BLemma  `termination`  THEN  Auto)

---

Home Index