---

Step * of Lemma cubical-lambda-subset

∀[X,phi,b:Top].  ((λb) ~ (λb))
BY
{ (Intros THEN RepUR ``cubical-lambda context-subset`` 0 THEN EqCD) }

---

Latex:

---

Latex:
\mforall{}[X,phi,b:Top].    ((\mlambda{}b)  \msim{}  (\mlambda{}b))


By

---

Latex:
(Intros  THEN  RepUR  ``cubical-lambda  context-subset``  0  THEN  EqCD)

---

Home Index