---

Step * 1 of Lemma union-product-disjoint


1. T : Type
2. S : Type
3. A : Type
4. B : Type
⊢ ¬A + B ⋂ T × S
BY
{ ((D 0 THEN Auto) THEN RenameVar `x' (-1)) }

1
1. T : Type
2. S : Type
3. A : Type
4. B : Type
5. x : A + B ⋂ T × S
⊢ False

---

Latex:

---

Latex:

1.  T  :  Type
2.  S  :  Type
3.  A  :  Type
4.  B  :  Type
\mvdash{}  \mneg{}A  +  B  \mcap{}  T  \mtimes{}  S


By

---

Latex:
((D  0  THEN  Auto)  THEN  RenameVar  `x'  (-1))

---

Home Index