Step 
*
 of Lemma 
unit-product-disjoint
∀[T,S:Type].  (¬Unit ⋂ T × S)
BY
 
{ Auto }
1
1. T : Type
2. S : Type
⊢ ¬Unit ⋂ T × S
 
Latex: 
Latex:
\mforall{}[T,S:Type].    (\mneg{}Unit  \mcap{}  T  \mtimes{}  S)
 By 
Latex:
Auto
Home
Index