---

Step * of Lemma same-cubical-type-zero-and-one

No Annotations
∀[G:j⊢]. ∀[A,B:{G, 0(𝔽) ⊢ _}]. ∀[i:{G ⊢ _:𝕀}].  G, ((i=0) ∧ (i=1)) ⊢ A = B
BY
{ (InstLemma `same-cubical-type-0` []
   THEN RepeatFor 3 (ParallelLast')
   THEN Auto
   THEN ParallelOp -2
   THEN SubsumeC ⌜{G, 0(𝔽) ⊢ _}⌝⋅
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A,B:\{G,  0(\mBbbF{})  \mvdash{}  \_\}].  \mforall{}[i:\{G  \mvdash{}  \_:\mBbbI{}\}].    G,  ((i=0)  \mwedge{}  (i=1))  \mvdash{}  A  =  B


By

---

Latex:
(InstLemma  `same-cubical-type-0`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  Auto
  THEN  ParallelOp  -2
  THEN  SubsumeC  \mkleeneopen{}\{G,  0(\mBbbF{})  \mvdash{}  \_\}\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index