---

Step * 1 of Lemma test-exists-elim


1. [A] : Type
2. [Q] : A ⟶ A ⟶ ℙ
3. x : A
4. b : A
⊢ ∃z:A × A. (Q[fst(z);snd(z)] ∧ (z = <x, b> ∈ (A × A))) ⇐⇒ Q[x;b] ∧ (x = x ∈ A)
BY
{ TACTIC:(RW (AddrC [1] (ExistsPairC ANDTHENC ReduceC ANDTHENC RepeatC ExistsElimC)) 0 THENA Auto) }

1
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)

---

Latex:

---

Latex:

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


By

---

Latex:
TACTIC:(RW  (AddrC  [1]  (ExistsPairC  ANDTHENC  ReduceC  ANDTHENC  RepeatC  ExistsElimC))  0  THENA  Auto)

---

Home Index