---

Step * of Lemma case-term-wf4

No Annotations
∀[Gamma:j⊢]. ∀[phi,psi:{Gamma ⊢ _:𝔽}]. ∀[A:{Gamma, phi ⊢ _}]. ∀[B:{Gamma, psi ⊢ _}]. ∀[u:{Gamma, phi ⊢ _:A}].
∀[v:{Gamma, psi ⊢ _:B}].
  ((u ∨ v) ∈ {Gamma, (phi ∨ psi) ⊢ _:(if phi then A else B)}) supposing 
     (Gamma, (phi ∧ psi) ⊢ u=v:A and 
     Gamma, (phi ∧ psi) ⊢ A = B)
BY
{ (RepeatFor 8 (Intro) THEN D 0) }

1
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. A : {Gamma, phi ⊢ _}
5. B : {Gamma, psi ⊢ _}
6. u : {Gamma, phi ⊢ _:A}
7. v : {Gamma, psi ⊢ _:B}
8. Gamma, (phi ∧ psi) ⊢ A = B
9. Gamma, (phi ∧ psi) ⊢ u=v:A
⊢ (u ∨ v) ∈ {Gamma, (phi ∨ psi) ⊢ _:(if phi then A else B)}

2
.....wf..... 
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. A : {Gamma, phi ⊢ _}
5. B : {Gamma, psi ⊢ _}
6. u : {Gamma, phi ⊢ _:A}
7. v : {Gamma, psi ⊢ _:B}
8. Gamma, (phi ∧ psi) ⊢ A = B
⊢ istype(Gamma, (phi ∧ psi) ⊢ u=v:A)

---

Latex:

---

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


By

---

Latex:
(RepeatFor  8  (Intro)  THEN  D  0)

---

Home Index