---

Step * of Lemma case-term-equal-right

No Annotations
∀[Gamma:j⊢]. ∀[phi,psi:{Gamma ⊢ _:𝔽}]. ∀[A:{Gamma, (phi ∨ psi) ⊢ _}]. ∀[u:{Gamma, phi ⊢ _:A}]. ∀[v:{Gamma, psi ⊢ _:A}].
  Gamma, psi ⊢ (u ∨ v)=v:A supposing Gamma, (phi ∧ psi) ⊢ u=v:A
BY
{ (Intros
   THEN UnfoldTopAb 0
   THEN Symmetry
   THEN (Assert ⌜v = (u ∨ v) ∈ (I:fset(ℕ) ⟶ a:Gamma, psi(I) ⟶ A(a))⌝⋅
   THENM (BLemma `cubical-term-equal` THEN Auto)
   )) }

1
.....assertion..... 
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. Gamma, (phi ∧ psi) ⊢ u=v:A
⊢ v = (u ∨ v) ∈ (I:fset(ℕ) ⟶ a:Gamma, psi(I) ⟶ A(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\}].
    Gamma,  psi  \mvdash{}  (u  \mvee{}  v)=v:A  supposing  Gamma,  (phi  \mwedge{}  psi)  \mvdash{}  u=v:A


By

---

Latex:
(Intros
  THEN  UnfoldTopAb  0
  THEN  Symmetry
  THEN  (Assert  \mkleeneopen{}v  =  (u  \mvee{}  v)\mkleeneclose{}\mcdot{}  THENM  (BLemma  `cubical-term-equal`  THEN  Auto)))

---

Home Index