---

Step * of Lemma csm-m-comp-1

No Annotations
∀[H:j⊢]. (m o [1(𝕀)] = 1(H.𝕀) ∈ H.𝕀 ij⟶ H.𝕀)
BY
{ (Intros
   THEN BLemma `csm-equal2`
   THEN Auto
   THEN RepUR ``cube-context-adjoin`` -1
   THEN D -1
   THEN RepUR ``cube-context-adjoin`` 0
   THEN (All (RWO "interval-type-at") THENA Auto)
   THEN All (RepUR ``interval-presheaf csm-id``)
   THEN CsmUnfolding
   THEN EqCD
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[H:j\mvdash{}].  (m  o  [1(\mBbbI{})]  =  1(H.\mBbbI{}))


By

---

Latex:
(Intros
  THEN  BLemma  `csm-equal2`
  THEN  Auto
  THEN  RepUR  ``cube-context-adjoin``  -1
  THEN  D  -1
  THEN  RepUR  ``cube-context-adjoin``  0
  THEN  (All  (RWO  "interval-type-at")  THENA  Auto)
  THEN  All  (RepUR  ``interval-presheaf  csm-id``)
  THEN  CsmUnfolding
  THEN  EqCD
  THEN  Auto)

---

Home Index