---

Step * of Lemma member-values-for-distinct2

∀[A,V:Type].  ∀eq:EqDecider(A). ∀L:(A × V) List. ∀v:V.  ((v ∈ values-for-distinct(eq;L)) ⇒ (∃a:A. (<a, v> ∈ L)))
BY
{ (Auto
   THEN Unfold `values-for-distinct` -1
   THEN (InstLemma `member_map` [⌜{a:A| (a ∈ remove-repeats(eq;map(λp.(fst(p));L)))} ⌝;⌜V⌝;
         ⌜remove-repeats(eq;map(λp.(fst(p));L))⌝;⌜v⌝;⌜λa.outl(apply-alist(eq;L;a))⌝]⋅
         THENA Auto
         )) }

1
1. A : Type
2. V : Type
3. eq : EqDecider(A)
4. L : (A × V) List
5. v : V
6. (v ∈ map(λa.outl(apply-alist(eq;L;a));remove-repeats(eq;map(λp.(fst(p));L))))
7. ∀a:A. ((a ∈ remove-repeats(eq;map(λp.(fst(p));L))) ∈ Type)
8. a : A
9. (a ∈ remove-repeats(eq;map(λp.(fst(p));L)))
⊢ ↑isl(apply-alist(eq;L;a))

2
1. [A] : Type
2. [V] : Type
3. eq : EqDecider(A)
4. L : (A × V) List
5. v : V
6. (v ∈ map(λa.outl(apply-alist(eq;L;a));remove-repeats(eq;map(λp.(fst(p));L))))
7. (v ∈ map(λa.outl(apply-alist(eq;L;a));remove-repeats(eq;map(λp.(fst(p));L))))
⇐⇒ ∃y:{a:A| (a ∈ remove-repeats(eq;map(λp.(fst(p));L)))} 
     ((y ∈ remove-repeats(eq;map(λp.(fst(p));L))) ∧ (v = ((λa.outl(apply-alist(eq;L;a))) y) ∈ V))
⊢ ∃a:A. (<a, v> ∈ L)

---

Latex:

---

Latex:
\mforall{}[A,V:Type].
    \mforall{}eq:EqDecider(A).  \mforall{}L:(A  \mtimes{}  V)  List.  \mforall{}v:V.
        ((v  \mmember{}  values-for-distinct(eq;L))  {}\mRightarrow{}  (\mexists{}a:A.  (<a,  v>  \mmember{}  L)))


By

---

Latex:
(Auto
  THEN  Unfold  `values-for-distinct`  -1
  THEN  (InstLemma  `member\_map`  [\mkleeneopen{}\{a:A|  (a  \mmember{}  remove-repeats(eq;map(\mlambda{}p.(fst(p));L)))\}  \mkleeneclose{};\mkleeneopen{}V\mkleeneclose{};
              \mkleeneopen{}remove-repeats(eq;map(\mlambda{}p.(fst(p));L))\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}\mlambda{}a.outl(apply-alist(eq;L;a))\mkleeneclose{}]\mcdot{}
              THENA  Auto
              ))

---

Home Index