---

Step * 2 1 of Lemma pairs-fpf_property


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)))
∧ (∀a:A. ((a ∈ remove-repeats(eq1;map(λp.(fst(p));L))) ⇐⇒ (a ∈ map(λp.(fst(p));L))))
⊢ ∀a:A. ((a ∈ remove-repeats(eq1;map(λp.(fst(p));L))) ⇐⇒ ∃b:B. (<a, b> ∈ L))
BY
{ ((((D (-1)) THEN (RWO "member_map" (-1))) THENA (Reduce 0 THEN Auto))
   THEN (Reduce (-1))
   THEN RepeatFor 2 (ParallelLast)
   THEN ExRepD) }

1
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. (a ∈ remove-repeats(eq1;map(λp.(fst(p));L)))@i
10. y : A × B
11. (y ∈ L)
12. a = (fst(y)) ∈ A
⊢ ∃b:B. (<a, b> ∈ L)

2
.....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))

---

Latex:



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)))
\mwedge{}  (\mforall{}a:A.  ((a  \mmember{}  remove-repeats(eq1;map(\mlambda{}p.(fst(p));L)))  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  map(\mlambda{}p.(fst(p));L))))
\mvdash{}  \mforall{}a:A.  ((a  \mmember{}  remove-repeats(eq1;map(\mlambda{}p.(fst(p));L)))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}b:B.  (<a,  b>  \mmember{}  L))


By

((((D  (-1))  THEN  (RWO  "member\_map"  (-1)))  THENA  (Reduce  0  THEN  Auto))
  THEN  (Reduce  (-1))
  THEN  RepeatFor  2  (ParallelLast)
  THEN  ExRepD)

---

Home Index