---

Step * 2 1 2 of Lemma pairs-fpf_property

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

---

Latex:

---

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


By

---

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

---

Home Index