---

Step * of Lemma values-for-distinct_wf

∀[A,V:Type]. ∀[eq:EqDecider(A)]. ∀[L:(A × V) List].  (values-for-distinct(eq;L) ∈ V List)
BY
{ (Auto THEN Unfold `values-for-distinct` 0) }

1
1. A : Type
2. V : Type
3. eq : EqDecider(A)
4. L : (A × V) List
⊢ map(λa.outl(apply-alist(eq;L;a));remove-repeats(eq;map(λp.(fst(p));L))) ∈ V List

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  Unfold  `values-for-distinct`  0)

---

Home Index