---

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

No Annotations
∀[Gamma:j⊢]. ∀[phi,psi:{Gamma ⊢ _:𝔽}]. ∀[A:{Gamma, (phi ∨ psi) ⊢ _}]. ∀[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
{ (RepeatFor 6 (Intro)
   THEN (Assert {Gamma, (phi ∨ psi) ⊢ _:A} ⊆r {Gamma, phi ⊢ _:A} BY
               (BLemma `subset-cubical-term` THEN Auto THEN BLemma `face-term-implies-subset` THEN Auto))
   THEN (Assert {Gamma, (phi ∨ psi) ⊢ _:A} ⊆r {Gamma, psi ⊢ _:A} BY
               (BLemma `subset-cubical-term` THEN Auto THEN BLemma `face-term-implies-subset` THEN Auto))
   THEN Intros
   THEN All (Unfold  `same-cubical-term`)) }

1
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. A : {Gamma, (phi ∨ psi) ⊢ _}
5. a : {Gamma, (phi ∨ psi) ⊢ _:A}
6. b : {Gamma, (phi ∨ psi) ⊢ _:A}
7. {Gamma, (phi ∨ psi) ⊢ _:A} ⊆r {Gamma, phi ⊢ _:A}
8. {Gamma, (phi ∨ psi) ⊢ _:A} ⊆r {Gamma, psi ⊢ _:A}
9. a = b ∈ {Gamma, psi ⊢ _:A}
10. a = b ∈ {Gamma, phi ⊢ _:A}
⊢ a = b ∈ {Gamma, (phi ∨ psi) ⊢ _:A}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[phi,psi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[A:\{Gamma,  (phi  \mvee{}  psi)  \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:
(RepeatFor  6  (Intro)
  THEN  (Assert  \{Gamma,  (phi  \mvee{}  psi)  \mvdash{}  \_:A\}  \msubseteq{}r  \{Gamma,  phi  \mvdash{}  \_:A\}  BY
                          (BLemma  `subset-cubical-term`
                            THEN  Auto
                            THEN  BLemma  `face-term-implies-subset`
                            THEN  Auto))
  THEN  (Assert  \{Gamma,  (phi  \mvee{}  psi)  \mvdash{}  \_:A\}  \msubseteq{}r  \{Gamma,  psi  \mvdash{}  \_:A\}  BY
                          (BLemma  `subset-cubical-term`
                            THEN  Auto
                            THEN  BLemma  `face-term-implies-subset`
                            THEN  Auto))
  THEN  Intros
  THEN  All  (Unfold    `same-cubical-term`))

---

Home Index