---

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


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))
BY
{ ((BLemma `isl-apply-alist` THENA Auto) THEN FLemma `member-remove-repeats` [-1] THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  V  :  Type
3.  eq  :  EqDecider(A)
4.  L  :  (A  \mtimes{}  V)  List
5.  v  :  V
6.  (v  \mmember{}  map(\mlambda{}a.outl(apply-alist(eq;L;a));remove-repeats(eq;map(\mlambda{}p.(fst(p));L))))
7.  \mforall{}a:A.  ((a  \mmember{}  remove-repeats(eq;map(\mlambda{}p.(fst(p));L)))  \mmember{}  Type)
8.  a  :  A
9.  (a  \mmember{}  remove-repeats(eq;map(\mlambda{}p.(fst(p));L)))
\mvdash{}  \muparrow{}isl(apply-alist(eq;L;a))


By

---

Latex:
((BLemma  `isl-apply-alist`  THENA  Auto)  THEN  FLemma  `member-remove-repeats`  [-1]  THEN  Auto)

---

Home Index