---

Step * of Lemma has-valueall-cons

∀[a,b:Base].  uiff(has-valueall(a) ∧ has-valueall(b);has-valueall([a / b]))
BY
{ (Unfold `has-valueall` 0
   THEN Auto
   THEN Try ((RecUnfold `evalall` 0
              THEN Reduce 0
              THEN RepeatFor 2 ((CallByValueReduce 0 THEN Auto))
              THEN Reduce 0
              THEN Auto))
   THEN (RecUnfold `evalall` (-1) THEN Reduce (-1) THEN RepeatFor 2 ((HasValueD (-1) THEN Auto THEN Thin (-1))))⋅) }

---

Latex:

---

Latex:
\mforall{}[a,b:Base].    uiff(has-valueall(a)  \mwedge{}  has-valueall(b);has-valueall([a  /  b]))


By

---

Latex:
(Unfold  `has-valueall`  0
  THEN  Auto
  THEN  Try  ((RecUnfold  `evalall`  0
                        THEN  Reduce  0
                        THEN  RepeatFor  2  ((CallByValueReduce  0  THEN  Auto))
                        THEN  Reduce  0
                        THEN  Auto))
  THEN  (RecUnfold  `evalall`  (-1)
              THEN  Reduce  (-1)
              THEN  RepeatFor  2  ((HasValueD  (-1)  THEN  Auto  THEN  Thin  (-1))))\mcdot{})

---

Home Index