Step * 2 1 of Lemma list-index-cmp-zero


1. Type
2. eq EqDecider(T)
3. List
4. Type
5. A ⟶ T
6. A
7. (f x ∈ L)
8. A
9. (f y ∈ L)
10. (f x) (f y) ∈ T
⊢ (outl(list-index(eq;L;f x)) outl(list-index(eq;L;f y))) 0 ∈ ℤ
BY
(StrongHypSubst (-1) THEN Auto THEN GenConclTerm ⌜outl(list-index(eq;L;f y))⌝⋅ THEN EAuto 1) }


Latex:


Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  T  List
4.  A  :  Type
5.  f  :  A  {}\mrightarrow{}  T
6.  x  :  A
7.  (f  x  \mmember{}  L)
8.  y  :  A
9.  (f  y  \mmember{}  L)
10.  (f  x)  =  (f  y)
\mvdash{}  (outl(list-index(eq;L;f  x))  -  outl(list-index(eq;L;f  y)))  =  0


By


Latex:
(StrongHypSubst  (-1)  0  THEN  Auto  THEN  GenConclTerm  \mkleeneopen{}outl(list-index(eq;L;f  y))\mkleeneclose{}\mcdot{}  THEN  EAuto  1)




Home Index