---

Step * of Lemma same-cubical-type-trivial_1

No Annotations
∀[X:j⊢]. ∀[i:{X ⊢ _:𝕀}]. ∀[x,y,B:Top].  X, (i=0), (i=1) ⊢ x=y:B
BY
{ (Auto THEN UnfoldTopAb  0 THEN BLemma `empty-context-subset-lemma3\'` THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[i:\{X  \mvdash{}  \_:\mBbbI{}\}].  \mforall{}[x,y,B:Top].    X,  (i=0),  (i=1)  \mvdash{}  x=y:B


By

---

Latex:
(Auto  THEN  UnfoldTopAb    0  THEN  BLemma  `empty-context-subset-lemma3\mbackslash{}'`  THEN  Auto)

---

Home Index