---

Step * 1 of Lemma CCC-product


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>)
BY
{ ((D 3 With ⌜λn,b. (R n <g n, b>)⌝  THENA Auto) THEN Reduce -1 THEN D -1 THEN Auto THEN RenameVar `h' (-1)) }

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

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  CCC(B)
4.  R  :  \mBbbN{}  {}\mrightarrow{}  (A  \mtimes{}  B)  {}\mrightarrow{}  \mBbbP{}
5.  \mforall{}g:\mBbbN{}  {}\mrightarrow{}  (A  \mtimes{}  B).  \mexists{}n:\mBbbN{}.  (R  n  (g  n))
6.  g  :  \mBbbN{}  {}\mrightarrow{}  A
\mvdash{}  \mexists{}n:\mBbbN{}.  \mforall{}b:B.  (R  n  <g  n,  b>)


By

---

Latex:
((D  3  With  \mkleeneopen{}\mlambda{}n,b.  (R  n  <g  n,  b>)\mkleeneclose{}    THENA  Auto)  THEN  Reduce  -1  THEN  D  -1  THEN  Auto  THEN  RenameVar  `h'\000C  (-1))

---

Home Index