---

Step * of Lemma partial-term-1-subset

∀[H,xx,u:Top].  (partial-term-1(H, xx;u) ~ partial-term-1(H;u))
BY
{ (RepUR ``partial-term-1 csm-id-adjoin csm-id`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[H,xx,u:Top].    (partial-term-1(H,  xx;u)  \msim{}  partial-term-1(H;u))


By

---

Latex:
(RepUR  ``partial-term-1  csm-id-adjoin  csm-id``  0  THEN  Auto)

---

Home Index