---

Step * of Lemma evalall-cons

∀a,b:Top.  (evalall([a / b]) ~ eval u = evalall(a) in eval v = evalall(b) in   [u / v])
BY
{ ((UnivCD THENA Auto) THEN RW (AddrC [1] RecUnfoldTopAbC) 0 THEN RepUR ``cons`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}a,b:Top.    (evalall([a  /  b])  \msim{}  eval  u  =  evalall(a)  in  eval  v  =  evalall(b)  in      [u  /  v])


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RW  (AddrC  [1]  RecUnfoldTopAbC)  0  THEN  RepUR  ``cons``  0  THEN  Auto)

---

Home Index