---

Step * of Lemma is-list-if-has-value-rec-subtype-unit

∀[t:Base]. (is-list-if-has-value-rec(t) ⊆r Unit)
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN RepUR ``is-list-if-has-value-rec is-list-if-has-value-fun`` (-1)
   THEN (With ⌜0⌝ (D (-1))⋅ THENA Auto)
   THEN AllReduce
   THEN DVar `y'
   THEN AutoSimpHyp Auto (-1)) }

---

Latex:

---

Latex:
\mforall{}[t:Base].  (is-list-if-has-value-rec(t)  \msubseteq{}r  Unit)


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  RepUR  ``is-list-if-has-value-rec  is-list-if-has-value-fun``  (-1)
  THEN  (With  \mkleeneopen{}0\mkleeneclose{}  (D  (-1))\mcdot{}  THENA  Auto)
  THEN  AllReduce
  THEN  DVar  `y'
  THEN  AutoSimpHyp  Auto  (-1))

---

Home Index