---

Step * of Lemma constant-A-open-box

∀Gamma,X,I,alpha:Top.  ∀[J,x,i:Top].  (A-open-box(Gamma;(X);I;alpha;J;x;i) ~ open_box(X;I;J;x;i))
BY
{ (Auto
   THEN RepUR ``A-open-box open_box`` 0
   THEN EqCD
   THEN RepUR ``A-face constant-cubical-type cubical-type-at I-face`` 0
   THEN Try (Trivial)
   THEN EqCD
   THEN RepUR ``A-face-name face-name`` 0
   THEN Try (Trivial)
   THEN RepUR ``A-adjacent-compatible adjacent-compatible`` 0
   THEN EqCD
   THEN Try (Trivial)
   THEN RepUR ``A-face-compatible face-compatible`` 0
   THEN RepUR ``cubical-type-ap-morph constant-cubical-type cubical-type-at`` 0
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}Gamma,X,I,alpha:Top.    \mforall{}[J,x,i:Top].    (A-open-box(Gamma;(X);I;alpha;J;x;i)  \msim{}  open\_box(X;I;J;x;i))


By

---

Latex:
(Auto
  THEN  RepUR  ``A-open-box  open\_box``  0
  THEN  EqCD
  THEN  RepUR  ``A-face  constant-cubical-type  cubical-type-at  I-face``  0
  THEN  Try  (Trivial)
  THEN  EqCD
  THEN  RepUR  ``A-face-name  face-name``  0
  THEN  Try  (Trivial)
  THEN  RepUR  ``A-adjacent-compatible  adjacent-compatible``  0
  THEN  EqCD
  THEN  Try  (Trivial)
  THEN  RepUR  ``A-face-compatible  face-compatible``  0
  THEN  RepUR  ``cubical-type-ap-morph  constant-cubical-type  cubical-type-at``  0
  THEN  Trivial)

---

Home Index