---

Step * of Lemma atom-test1

     (Unhideable token semantics in effect)

'xxx'1 =a1 'yyy'1 = ff
BY
{ Unfold `eq_atom` 0  }

1
     (Unhideable token semantics in effect)

if 'xxx'1=1 'yyy'1 then tt else ff = ff

---

Latex:

---

Latex:
          (Unhideable  token  semantics  in  effect)

'xxx'1  =a1  'yyy'1  =  ff


By

---

Latex:
Unfold  `eq\_atom`  0 

---

Home Index