---

Step * of Lemma cubical-lambda-subset2

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

---

Latex:

---

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


By

---

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

---

Home Index