---

Step * of Lemma islist-list

∀[T:Type]. ∀[t:T List].  islist(t)
BY
{ (RepUR ``islist eval_list`` 0
   THEN InductionOnList
   THEN Reduce 0
   THEN Try (CallByValueReduce 0)
   THEN Auto
   THEN RepUR ``has-value`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[t:T  List].    islist(t)


By

---

Latex:
(RepUR  ``islist  eval\_list``  0
  THEN  InductionOnList
  THEN  Reduce  0
  THEN  Try  (CallByValueReduce  0)
  THEN  Auto
  THEN  RepUR  ``has-value``  0
  THEN  Auto)

---

Home Index