---

Step * of Lemma rev_app_cons_lemma

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

1
1. bs : Top@i
2. as : Top@i
3. a : Top@i
⊢ rev([a / as]) + bs ~ rev(as) + [a / bs]

---

Latex:

---

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


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index