---

Step * 2 1 2 of Lemma pairs-fpf_property

.....antecedent..... 
1. [A] : Type
2. [B] : Type
3. eq1 : EqDecider(A)@i
4. eq2 : EqDecider(B)@i
5. L : (A × B) List@i
6. no_repeats(A;fpf-domain(fpf(L)))
7. no_repeats(A;remove-repeats(eq1;map(λp.(fst(p));L)))
8. a : A@i
9. ∃b:B. (<a, b> ∈ L)@i
⊢ ∃y:A × B. ((y ∈ L) ∧ (a = (fst(y)) ∈ A))
BY
{ (ExRepD THEN (InstConcl [⌈<a, b>⌉])⋅ THEN Reduce 0 THEN Auto) }

---

Latex:


.....antecedent..... 
1.  [A]  :  Type
2.  [B]  :  Type
3.  eq1  :  EqDecider(A)@i
4.  eq2  :  EqDecider(B)@i
5.  L  :  (A  \mtimes{}  B)  List@i
6.  no\_repeats(A;fpf-domain(fpf(L)))
7.  no\_repeats(A;remove-repeats(eq1;map(\mlambda{}p.(fst(p));L)))
8.  a  :  A@i
9.  \mexists{}b:B.  (<a,  b>  \mmember{}  L)@i
\mvdash{}  \mexists{}y:A  \mtimes{}  B.  ((y  \mmember{}  L)  \mwedge{}  (a  =  (fst(y))))


By

(ExRepD  THEN  (InstConcl  [\mkleeneopen{}<a,  b>\mkleeneclose{}])\mcdot{}  THEN  Reduce  0  THEN  Auto)

---

Home Index