---

Step * 1 1 of Lemma test-exists-elim


1. [A] : Type
2. [Q] : A ⟶ A ⟶ ℙ
3. x : A
4. b : A
⊢ Q[x;b] ∧ (<x, b> = <x, b> ∈ (A × A)) ⇐⇒ Q[x;b] ∧ (x = x ∈ A)
BY
{ TACTIC:Auto }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [Q]  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
3.  x  :  A
4.  b  :  A
\mvdash{}  Q[x;b]  \mwedge{}  (<x,  b>  =  <x,  b>)  \mLeftarrow{}{}\mRightarrow{}  Q[x;b]  \mwedge{}  (x  =  x)


By

---

Latex:
TACTIC:Auto

---

Home Index