---

Step * of Lemma glue-type-subset

No Annotations
∀[Gamma,A,phi,T,w,xx:Top].  (Gamma, xx ⊢ Glue [phi ⊢→ (T;w)] A ~ Gamma ⊢ Glue [phi ⊢→ (T;w)] A)
BY
{ (Intros THEN RepUR ``glue-type glue-cube glue-morph glue-equations context-subset`` 0 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma,A,phi,T,w,xx:Top].    (Gamma,  xx  \mvdash{}  Glue  [phi  \mvdash{}\mrightarrow{}  (T;w)]  A  \msim{}  Gamma  \mvdash{}  Glue  [phi  \mvdash{}\mrightarrow{}  (T;w)]  A)


By

---

Latex:
(Intros  THEN  RepUR  ``glue-type  glue-cube  glue-morph  glue-equations  context-subset``  0  THEN  Auto)

---

Home Index