---

Step * of Lemma case-term-wf3

No Annotations
∀[Gamma:j⊢]. ∀[phi,psi:{Gamma ⊢ _:𝔽}]. ∀[A:{Gamma, (phi ∨ psi) ⊢ _}]. ∀[v:{Gamma, psi ⊢ _:A}].
∀[u:{Gamma, phi ⊢ _:A[psi |⟶ v]}].
  ((u ∨ v) ∈ {t:{Gamma, (phi ∨ psi) ⊢ _:A}| Gamma, psi ⊢ t=v:A} )
BY
{ (Intros THEN MemTypeCD) }

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

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

3
.....wf..... 
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. A : {Gamma, (phi ∨ psi) ⊢ _}
5. v : {Gamma, psi ⊢ _:A}
6. u : {Gamma, phi ⊢ _:A[psi |⟶ v]}
7. t : {Gamma, (phi ∨ psi) ⊢ _:A}
⊢ istype(Gamma, psi ⊢ t=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{}  \{t:\{Gamma,  (phi  \mvee{}  psi)  \mvdash{}  \_:A\}|  Gamma,  psi  \mvdash{}  t=v:A\}  )


By

---

Latex:
(Intros  THEN  MemTypeCD)

---

Home Index