---

Step * of Lemma ut1-test_wf

     (Unhideable token semantics in effect)

∀[x:Top + Top]. (ut1-test{$aaa,$bbb}(x) ∈ Atom1)
BY
{ (ProveWfLemma THEN Unfold `member` 0 THEN Refine `token1Equality` []) }

---

Latex:

---

Latex:
          (Unhideable  token  semantics  in  effect)

\mforall{}[x:Top  +  Top].  (ut1-test\{\$aaa,\$bbb\}(x)  \mmember{}  Atom1)


By

---

Latex:
(ProveWfLemma  THEN  Unfold  `member`  0  THEN  Refine  `token1Equality`  [])

---

Home Index