---

Step * of Lemma list-index-cmp-zero

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List]. ∀[A:Type]. ∀[f:A ⟶ T]. ∀[x,y:{x:A| (f x ∈ L)} ].
  uiff((list-index-cmp(eq;L;f) x y) = 0 ∈ ℤ;(f x) = (f y) ∈ T)
BY
{ TACTIC:Auto }

1
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. A : Type
5. f : A ⟶ T
6. x : {x:A| (f x ∈ L)} 
7. y : {x:A| (f x ∈ L)} 
8. (list-index-cmp(eq;L;f) x y) = 0 ∈ ℤ
⊢ (f x) = (f y) ∈ T

2
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. A : Type
5. f : A ⟶ T
6. x : {x:A| (f x ∈ L)} 
7. y : {x:A| (f x ∈ L)} 
8. (f x) = (f y) ∈ T
⊢ (list-index-cmp(eq;L;f) x y) = 0 ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[L:T  List].  \mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  T].  \mforall{}[x,y:\{x:A|  (f  x  \mmember{}  L)\}  ].
    uiff((list-index-cmp(eq;L;f)  x  y)  =  0;(f  x)  =  (f  y))


By

---

Latex:
TACTIC:Auto

---

Home Index