---

Step * of Lemma values-for-distinct-nil

∀[A,V:Type]. ∀[eq:EqDecider(A)]. ∀[L:(A × V) List].
  uiff(values-for-distinct(eq;L) = [] ∈ (V List);L = [] ∈ ((A × V) List))
BY
{ (InstLemma `values-for-distinct-property` [] THEN RepeatFor 4 (ParallelLast') THEN Auto) }

1
1. A : Type
2. V : Type
3. eq : EqDecider(A)
4. L : (A × V) List
5. ||values-for-distinct(eq;L)|| = ||remove-repeats(eq;map(λp.(fst(p));L))|| ∈ ℤ
6. ∀i:ℕ||remove-repeats(eq;map(λp.(fst(p));L))||
     (<remove-repeats(eq;map(λp.(fst(p));L))[i], values-for-distinct(eq;L)[i]> ∈ L)
7. values-for-distinct(eq;L) = [] ∈ (V List)
⊢ L = [] ∈ ((A × V) List)

2
1. A : Type
2. V : Type
3. eq : EqDecider(A)
4. L : (A × V) List
5. ||values-for-distinct(eq;L)|| = ||remove-repeats(eq;map(λp.(fst(p));L))|| ∈ ℤ
6. ∀i:ℕ||remove-repeats(eq;map(λp.(fst(p));L))||
     (<remove-repeats(eq;map(λp.(fst(p));L))[i], values-for-distinct(eq;L)[i]> ∈ L)
7. L = [] ∈ ((A × V) List)
⊢ values-for-distinct(eq;L) = [] ∈ (V List)

---

Latex:

---

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


By

---

Latex:
(InstLemma  `values-for-distinct-property`  []  THEN  RepeatFor  4  (ParallelLast')  THEN  Auto)

---

Home Index