---

Step * of Lemma csm-Kan-unit-cube-id

∀I:Cname List. ∀x:{unit-cube(I) ⊢ _(Kan)}.  ((x)unit-cube-map(1) = x ∈ {unit-cube(I) ⊢ _(Kan)})
BY
{ (Auto THEN Subst ⌜unit-cube-map(1) = 1(unit-cube(I)) ∈ unit-cube(I) ⟶ unit-cube(I)⌝ 0⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}I:Cname  List.  \mforall{}x:\{unit-cube(I)  \mvdash{}  \_(Kan)\}.    ((x)unit-cube-map(1)  =  x)


By

---

Latex:
(Auto  THEN  Subst  \mkleeneopen{}unit-cube-map(1)  =  1(unit-cube(I))\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index