---

Step * of Lemma has-valueall-pair

∀[a,b:Base].  uiff(has-valueall(<a, b>);has-valueall(a) ∧ has-valueall(b))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `has-valueall` 0
   THEN RWO "evalall-pair" 0
   THEN Auto
   THEN Try (RepeatFor 2 ((HasValueD 3 THEN Auto)))
   THEN RW (AddrC [1;1] RecUnfoldTopAbC) 0
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN Auto
   THEN RepUR ``has-value`` 0
   THEN RW (AddrC [2] (TagC (mk_tag_term 1))) 0
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `has-valueall`  0
  THEN  RWO  "evalall-pair"  0
  THEN  Auto
  THEN  Try  (RepeatFor  2  ((HasValueD  3  THEN  Auto)))
  THEN  RW  (AddrC  [1;1]  RecUnfoldTopAbC)  0
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  Auto
  THEN  RepUR  ``has-value``  0
  THEN  RW  (AddrC  [2]  (TagC  (mk\_tag\_term  1)))  0
  THEN  Auto)

---

Home Index