---

Step * of Lemma case-term-same2

No Annotations
∀[Gamma:j⊢]. ∀[phi,psi:{Gamma ⊢ _:𝔽}]. ∀[A:{Gamma ⊢ _}]. ∀[u:{Gamma, phi ⊢ _:A}]. ∀[v:{Gamma, psi ⊢ _:A}].
∀[w:{Gamma ⊢ _:A}].
  (Gamma, (phi ∨ psi) ⊢ (u ∨ v)=w:A) supposing (Gamma, phi ⊢ u=w:A and Gamma, psi ⊢ v=w:A)
BY
{ (Unfold `same-cubical-term` 0
   THEN Intros
   THEN Symmetry
   THEN (CubicalTermEqual THENA Auto)
   THEN RepUR ``case-term`` 0
   THEN Fold `cubical-term-at` 0) }

1
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. A : {Gamma ⊢ _}
5. u : {Gamma, phi ⊢ _:A}
6. v : {Gamma, psi ⊢ _:A}
7. w : {Gamma ⊢ _:A}
8. v = w ∈ {Gamma, psi ⊢ _:A}
9. u = w ∈ {Gamma, phi ⊢ _:A}
10. I : fset(ℕ)
11. a : Gamma, (phi ∨ psi)(I)
⊢ w(a) = if (phi(a)==1) then u(a) else v(a) fi  ∈ A(a)

---

Latex:

---

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


By

---

Latex:
(Unfold  `same-cubical-term`  0
  THEN  Intros
  THEN  Symmetry
  THEN  (CubicalTermEqual  THENA  Auto)
  THEN  RepUR  ``case-term``  0
  THEN  Fold  `cubical-term-at`  0)

---

Home Index