---

Step * of Lemma rev_app_nil_lemma

∀bs:Top. (rev([]) + bs ~ bs)
BY
{ (UnivCD THENA Auto) }

1
1. bs : Top@i
⊢ rev([]) + bs ~ bs

---

Latex:

---

Latex:
\mforall{}bs:Top.  (rev([])  +  bs  \msim{}  bs)


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index