---

Step * of Lemma act_locl_lemma

∀a:Top. (act(locl(a)) ~ a)
BY
{ (UnivCD THENA Auto) }

1
1. a : Top@i
⊢ act(locl(a)) ~ a

---

Latex:


\mforall{}a:Top.  (act(locl(a))  \msim{}  a)


By

(UnivCD  THENA  Auto)

---

Home Index