---

Step * of Lemma case-term-equality-right

No Annotations
∀[Gamma:j⊢]. ∀[phi,psi:{Gamma ⊢ _:𝔽}]. ∀[A:{Gamma, (phi ∨ psi) ⊢ _}]. ∀[u:{Gamma, phi ⊢ _:A}]. ∀[v:{Gamma, psi ⊢ _:A}].
  ∀[x:{Gamma, (phi ∨ psi) ⊢ _:A}]. Gamma, psi ⊢ v=x:A supposing Gamma, (phi ∨ psi) ⊢ (u ∨ v)=x:A 
  supposing Gamma, (phi ∧ psi) ⊢ u=v:A
BY
{ (InstLemma `case-term-equal-right` []
   THEN RepeatFor 6 (ParallelLast')
   THEN Intro
   THEN (InstLemma `case-term_wf` [⌜Gamma⌝;⌜phi⌝;⌜psi⌝;⌜A⌝;⌜u⌝;⌜v⌝]⋅ THENA Auto)
   THEN Intros
   THEN ThinTrivial
   THEN All (Unfold  `same-cubical-term`)) }

1
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. A : {Gamma, (phi ∨ psi) ⊢ _}
5. u : {Gamma, phi ⊢ _:A}
6. v : {Gamma, psi ⊢ _:A}
7. u = v ∈ {Gamma, (phi ∧ psi) ⊢ _:A}
8. (u ∨ v) ∈ {Gamma, (phi ∨ psi) ⊢ _:A}
9. x : {Gamma, (phi ∨ psi) ⊢ _:A}
10. (u ∨ v) = x ∈ {Gamma, (phi ∨ psi) ⊢ _:A}
11. (u ∨ v) = v ∈ {Gamma, psi ⊢ _:A}
⊢ v = x ∈ {Gamma, psi ⊢ _:A}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[phi,psi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[A:\{Gamma,  (phi  \mvee{}  psi)  \mvdash{}  \_\}].  \mforall{}[u:\{Gamma,  phi  \mvdash{}  \_:A\}].
\mforall{}[v:\{Gamma,  psi  \mvdash{}  \_:A\}].
    \mforall{}[x:\{Gamma,  (phi  \mvee{}  psi)  \mvdash{}  \_:A\}].  Gamma,  psi  \mvdash{}  v=x:A  supposing  Gamma,  (phi  \mvee{}  psi)  \mvdash{}  (u  \mvee{}  v)=x:A 
    supposing  Gamma,  (phi  \mwedge{}  psi)  \mvdash{}  u=v:A


By

---

Latex:
(InstLemma  `case-term-equal-right`  []
  THEN  RepeatFor  6  (ParallelLast')
  THEN  Intro
  THEN  (InstLemma  `case-term\_wf`  [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{};\mkleeneopen{}psi\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Intros
  THEN  ThinTrivial
  THEN  All  (Unfold    `same-cubical-term`))

---

Home Index