---

Step * 2 1 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)))
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)
BY
{ ((InstConcl [⌈snd(y)⌉])⋅
   THEN Reduce 0
   THEN Auto
   THEN (NthHypEq (-2))
   THEN EqCD
   THEN Auto
   THEN DVar `y'
   THEN All Reduce
   THEN EqCD
   THEN Auto) }

---

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)))
8.  a  :  A@i
9.  (a  \mmember{}  remove-repeats(eq1;map(\mlambda{}p.(fst(p));L)))@i
10.  y  :  A  \mtimes{}  B
11.  (y  \mmember{}  L)
12.  a  =  (fst(y))
\mvdash{}  \mexists{}b:B.  (<a,  b>  \mmember{}  L)


By

((InstConcl  [\mkleeneopen{}snd(y)\mkleeneclose{}])\mcdot{}
  THEN  Reduce  0
  THEN  Auto
  THEN  (NthHypEq  (-2))
  THEN  EqCD
  THEN  Auto
  THEN  DVar  `y'
  THEN  All  Reduce
  THEN  EqCD
  THEN  Auto)

---

Home Index