---

Step * of Lemma case-term_wf2

No Annotations
∀[Gamma:j⊢]. ∀[phi,psi:{Gamma ⊢ _:𝔽}]. ∀[A:{Gamma, (phi ∨ psi) ⊢ _}]. ∀[v:{Gamma, psi ⊢ _:A}].
∀[u:{Gamma, phi ⊢ _:A[psi |⟶ v]}].
  ((u ∨ v) ∈ {Gamma, (phi ∨ psi) ⊢ _:A})
BY
{ (InstLemma `case-term_wf` []
   THEN RepeatFor 4 (ParallelLast')
   THEN (Assert Gamma, psi ⊢ A BY
               Auto)
   THEN Intro
   THEN Thin(-2)
   THEN (Assert Gamma, phi ⊢ A BY
               Auto)
   THEN Intro
   THEN Thin(-2)
   THEN (BHyp -3 THENW Auto)) }

1
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. A : {Gamma, (phi ∨ psi) ⊢ _}
5. ∀[u:{Gamma, phi ⊢ _:A}]. ∀[v:{Gamma, psi ⊢ _:A}].
     (u ∨ v) ∈ {Gamma, (phi ∨ psi) ⊢ _:A} supposing Gamma, (phi ∧ psi) ⊢ u=v:A
6. v : {Gamma, psi ⊢ _:A}
7. u : {Gamma, phi ⊢ _:A[psi |⟶ v]}
⊢ Gamma, (phi ∧ psi) ⊢ u=v:A

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[phi,psi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[A:\{Gamma,  (phi  \mvee{}  psi)  \mvdash{}  \_\}].  \mforall{}[v:\{Gamma,  psi  \mvdash{}  \_:A\}].
\mforall{}[u:\{Gamma,  phi  \mvdash{}  \_:A[psi  |{}\mrightarrow{}  v]\}].
    ((u  \mvee{}  v)  \mmember{}  \{Gamma,  (phi  \mvee{}  psi)  \mvdash{}  \_:A\})


By

---

Latex:
(InstLemma  `case-term\_wf`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  (Assert  Gamma,  psi  \mvdash{}  A  BY
                          Auto)
  THEN  Intro
  THEN  Thin(-2)
  THEN  (Assert  Gamma,  phi  \mvdash{}  A  BY
                          Auto)
  THEN  Intro
  THEN  Thin(-2)
  THEN  (BHyp  -3  THENW  Auto))

---

Home Index