---

Step * of Lemma es-dt-ap

∀[da,l,tg:Top].  (dt(l;da)(tg) ~ da(rcv(l,tg)))
BY
{ (RepUR ``fpf-all es-dt compose-fpf fpf-dom fpf-ap`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[da,l,tg:Top].    (dt(l;da)(tg)  \msim{}  da(rcv(l,tg)))


By

---

Latex:
(RepUR  ``fpf-all  es-dt  compose-fpf  fpf-dom  fpf-ap``  0  THEN  Auto)

---

Home Index