Step
*
of Lemma
exists-product3
∀[A,B,C,D:Type]. ∀P:(A × B × C × D) ⟶ ℙ'. {∃x:A × B × C × D. P[x]
⇐⇒ ∃a:A. ∃b:B. ∃c:C. ∃d:D. P[<a, b, c, d>]}
BY
{ (Unfold `guard` 0 THEN ((UnivCD THENA Auto) THEN (RWW "exists-product1" 0 THENA Auto) THEN Auto)) }
Latex:
Latex:
\mforall{}[A,B,C,D:Type].
\mforall{}P:(A \mtimes{} B \mtimes{} C \mtimes{} D) {}\mrightarrow{} \mBbbP{}'. \{\mexists{}x:A \mtimes{} B \mtimes{} C \mtimes{} D. P[x] \mLeftarrow{}{}\mRightarrow{} \mexists{}a:A. \mexists{}b:B. \mexists{}c:C. \mexists{}d:D. P[<a, b, c, d>]\}
By
Latex:
(Unfold `guard` 0 THEN ((UnivCD THENA Auto) THEN (RWW "exists-product1" 0 THENA Auto) THEN Auto))
Home
Index