---

Step * of Lemma evalall-atom

∀[x:Atom]. (evalall(x) ~ x)
BY
{ (Auto
   THEN RW (AddrC [2] (RecUnfoldC `evalall`)) 0
   THEN (CallByValueReduce 0 THENA (Unfold `has-value` 0 THEN Refine_callbyvalueAtom THEN Auto))) }

1
1. x : Atom
⊢ if x is a pair then let a,b = x 
                      in eval a' = evalall(a) in
                         eval b' = evalall(b) in
                           <a', b'> otherwise if x is inl then eval y = evalall(outl(x)) in
                                                               inl y
                                              else if x is inr then eval y = evalall(outr(x)) in
                                                                    inr y 
                                                   else x
= x
∈ Atom

---

Latex:

---

Latex:
\mforall{}[x:Atom].  (evalall(x)  \msim{}  x)


By

---

Latex:
(Auto
  THEN  RW  (AddrC  [2]  (RecUnfoldC  `evalall`))  0
  THEN  (CallByValueReduce  0  THENA  (Unfold  `has-value`  0  THEN  Refine\_callbyvalueAtom  THEN  Auto)))

---

Home Index