---

Step * of Lemma case-term_wf

No Annotations
∀[Gamma:j⊢]. ∀[phi,psi:{Gamma ⊢ _:𝔽}]. ∀[A:{Gamma, (phi ∨ psi) ⊢ _}]. ∀[u:{Gamma, phi ⊢ _:A}]. ∀[v:{Gamma, psi ⊢ _:A}].
  (u ∨ v) ∈ {Gamma, (phi ∨ psi) ⊢ _:A} supposing Gamma, (phi ∧ psi) ⊢ u=v:A
BY
{ (RepeatFor 4 (Intro)
   THEN ((Assert Gamma, phi ⊢ A BY Auto) THEN Intro)
   THEN ((Assert Gamma, psi ⊢ A BY Auto) THEN Intro)
   THEN (Assert Gamma, (phi ∧ psi) ⊢ A BY
               Auto)
   THEN Intro
   THEN Thin (-2)
   THEN Thin (-3)
   THEN Thin (-4)
   THEN MemTypeCD
   THEN Auto) }

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. Gamma, (phi ∧ psi) ⊢ u=v:A
⊢ (u ∨ v) ∈ I:fset(ℕ) ⟶ a:Gamma, (phi ∨ psi)(I) ⟶ A(a)

2
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
8. I : fset(ℕ)
9. J : fset(ℕ)
10. f : J ⟶ I
11. a : Gamma, (phi ∨ psi)(I)
⊢ ((u ∨ v) I a a f) = ((u ∨ v) J f(a)) ∈ A(f(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\}].
    (u  \mvee{}  v)  \mmember{}  \{Gamma,  (phi  \mvee{}  psi)  \mvdash{}  \_:A\}  supposing  Gamma,  (phi  \mwedge{}  psi)  \mvdash{}  u=v:A


By

---

Latex:
(RepeatFor  4  (Intro)
  THEN  ((Assert  Gamma,  phi  \mvdash{}  A  BY  Auto)  THEN  Intro)
  THEN  ((Assert  Gamma,  psi  \mvdash{}  A  BY  Auto)  THEN  Intro)
  THEN  (Assert  Gamma,  (phi  \mwedge{}  psi)  \mvdash{}  A  BY
                          Auto)
  THEN  Intro
  THEN  Thin  (-2)
  THEN  Thin  (-3)
  THEN  Thin  (-4)
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index