---

Step * 1 of Lemma exists-pair


1. [A] : Type
2. [B] : Type
3. [P] : (A × B) ⟶ ℙ
4. p : A × B@i
5. P[p]@i
⊢ ∃a:A. ∃b:B. P[<a, b>]
BY
{ (D (-2) THEN InstConcl [⌜p1⌝;⌜p2⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  [P]  :  (A  \mtimes{}  B)  {}\mrightarrow{}  \mBbbP{}
4.  p  :  A  \mtimes{}  B@i
5.  P[p]@i
\mvdash{}  \mexists{}a:A.  \mexists{}b:B.  P[<a,  b>]


By

---

Latex:
(D  (-2)  THEN  InstConcl  [\mkleeneopen{}p1\mkleeneclose{};\mkleeneopen{}p2\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index