---

Step * of Lemma cubical-term-eqcd

No Annotations
∀[X:j⊢]. ∀[A,B:{X ⊢ _}].  {X ⊢ _:A} = {X ⊢ _:B} ∈ 𝕌{[i | j']} supposing A = B ∈ {X ⊢ _}
BY
{ Auto }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[A,B:\{X  \mvdash{}  \_\}].    \{X  \mvdash{}  \_:A\}  =  \{X  \mvdash{}  \_:B\}  supposing  A  =  B


By

---

Latex:
Auto

---

Home Index