---

Step * of Lemma same-cubical-term-by-cases2

No Annotations
∀[Gamma:j⊢]. ∀[phi,psi:{Gamma ⊢ _:𝔽}]. ∀[A:{Gamma ⊢ _}]. ∀[a,b:{Gamma, (phi ∨ psi) ⊢ _:A}].
  (Gamma, (phi ∨ psi) ⊢ a=b:A) supposing (Gamma, phi ⊢ a=b:A and Gamma, psi ⊢ a=b:A)
BY
{ (InstLemma `same-cubical-term-by-cases` [] THEN RepeatFor 4 (ParallelLast')) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[phi,psi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[a,b:\{Gamma,  (phi  \mvee{}  psi)  \mvdash{}  \_:A\}].
    (Gamma,  (phi  \mvee{}  psi)  \mvdash{}  a=b:A)  supposing  (Gamma,  phi  \mvdash{}  a=b:A  and  Gamma,  psi  \mvdash{}  a=b:A)


By

---

Latex:
(InstLemma  `same-cubical-term-by-cases`  []  THEN  RepeatFor  4  (ParallelLast'))

---

Home Index