---

Step * of Lemma member-values-for-distinct

∀[A,V:Type].
  ∀eq:EqDecider(A). ∀L:(A × V) List. ∀a:A.
    ((a ∈ map(λp.(fst(p));L)) ⇒ (∃v:V. ((v ∈ values-for-distinct(eq;L)) ∧ (<a, v> ∈ L))))
BY
{ (Auto THEN (UsingVars [`eq'] (FLemma `member-remove-repeats` [-1])⋅ THENA Auto)) }

1
1. [A] : Type
2. [V] : Type
3. eq : EqDecider(A)@i
4. L : (A × V) List@i
5. a : A@i
6. (a ∈ map(λp.(fst(p));L))@i
7. (a ∈ remove-repeats(eq;map(λp.(fst(p));L)))
⊢ ∃v:V. ((v ∈ values-for-distinct(eq;L)) ∧ (<a, v> ∈ L))

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (UsingVars  [`eq']  (FLemma  `member-remove-repeats`  [-1])\mcdot{}  THENA  Auto))

---

Home Index