---

Step * 1 of Lemma member-values-for-distinct


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))
BY
{ ((InstLemma `values-for-distinct-property` [⌜A⌝;⌜V⌝;⌜eq⌝;⌜L⌝]⋅ THEN Auto)
   THEN RepeatFor 2 (D -3)
   THEN (InstHyp [⌜i⌝] (-1)⋅ THENA Auto)
   THEN InstConcl [⌜values-for-distinct(eq;L)[i]⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [V]  :  Type
3.  eq  :  EqDecider(A)@i
4.  L  :  (A  \mtimes{}  V)  List@i
5.  a  :  A@i
6.  (a  \mmember{}  map(\mlambda{}p.(fst(p));L))@i
7.  (a  \mmember{}  remove-repeats(eq;map(\mlambda{}p.(fst(p));L)))
\mvdash{}  \mexists{}v:V.  ((v  \mmember{}  values-for-distinct(eq;L))  \mwedge{}  (<a,  v>  \mmember{}  L))


By

---

Latex:
((InstLemma  `values-for-distinct-property`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}V\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  RepeatFor  2  (D  -3)
  THEN  (InstHyp  [\mkleeneopen{}i\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  InstConcl  [\mkleeneopen{}values-for-distinct(eq;L)[i]\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index