Step
*
of Lemma
singleton-type-product
∀[A,B:Type]. (singleton-type(A)
⇒ singleton-type(B)
⇒ singleton-type(A × B))
BY
{ (Unfold `singleton-type` 0 THEN Auto THEN ExRepD THEN RenameVar `b' (-2) THEN With ⌜<a1, b>⌝ (D 0)⋅ THEN Auto) }
1
1. A : Type
2. B : Type
3. a1 : A@i
4. ∀a':A. (a' = a1 ∈ A)@i
5. b : B@i
6. ∀a':B. (a' = b ∈ B)@i
7. a' : A × B@i
⊢ a' = <a1, b> ∈ (A × B)
Latex:
Latex:
\mforall{}[A,B:Type]. (singleton-type(A) {}\mRightarrow{} singleton-type(B) {}\mRightarrow{} singleton-type(A \mtimes{} B))
By
Latex:
(Unfold `singleton-type` 0
THEN Auto
THEN ExRepD
THEN RenameVar `b' (-2)
THEN With \mkleeneopen{}<a1, b>\mkleeneclose{} (D 0)\mcdot{}
THEN Auto)
Home
Index