---

Step * of Lemma union-product-disjoint

∀[T,S,A,B:Type].  (¬A + B ⋂ T × S)
BY
{ Auto }

1
1. T : Type
2. S : Type
3. A : Type
4. B : Type
⊢ ¬A + B ⋂ T × S

---

Latex:

---

Latex:
\mforall{}[T,S,A,B:Type].    (\mneg{}A  +  B  \mcap{}  T  \mtimes{}  S)


By

---

Latex:
Auto

---

Home Index