---

Step * of Lemma CCC-product

∀A,B:Type.  (CCC(A) ⇒ CCC(B) ⇒ CCC(A × B))
BY
{ ((Auto THEN D 0)
   THEN Auto
   THEN (D 3 With ⌜λn,a. ∀b:B. (R n <a, b>)⌝  THENA Auto)
   THEN Reduce -1
   THEN (D -1 THENM (ParallelLast THEN Auto THEN D -1 THEN Auto))
   THEN Auto) }

1
1. A : Type
2. B : Type
3. CCC(B)
4. R : ℕ ⟶ (A × B) ⟶ ℙ
5. ∀g:ℕ ⟶ (A × B). ∃n:ℕ. (R n (g n))
6. g : ℕ ⟶ A
⊢ ∃n:ℕ. ∀b:B. (R n <g n, b>)

---

Latex:

---

Latex:
\mforall{}A,B:Type.    (CCC(A)  {}\mRightarrow{}  CCC(B)  {}\mRightarrow{}  CCC(A  \mtimes{}  B))


By

---

Latex:
((Auto  THEN  D  0)
  THEN  Auto
  THEN  (D  3  With  \mkleeneopen{}\mlambda{}n,a.  \mforall{}b:B.  (R  n  <a,  b>)\mkleeneclose{}    THENA  Auto)
  THEN  Reduce  -1
  THEN  (D  -1  THENM  (ParallelLast  THEN  Auto  THEN  D  -1  THEN  Auto))
  THEN  Auto)

---

Home Index