---

Step * of Lemma l_index_hd

∀[T:Type]. ∀[dT:EqDecider(T)]. ∀[L:T List].  index(L;hd(L)) ~ 0 supposing ¬↑null(L)
BY
{ ((UnivCD THENA Auto)
   THEN DVar `L'
   THEN All Reduce
   THEN Try (Complete (Auto))
   THEN RepUR ``l_index eqof`` 0
   THEN Unfold `mu` 0) }

1
1. T : Type
2. dT : EqDecider(T)
3. u : T
4. v : T List
5. ¬False
⊢ mu-ge(λi.(dT u [u / v][i]);0) ~ 0

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[dT:EqDecider(T)].  \mforall{}[L:T  List].    index(L;hd(L))  \msim{}  0  supposing  \mneg{}\muparrow{}null(L)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  DVar  `L'
  THEN  All  Reduce
  THEN  Try  (Complete  (Auto))
  THEN  RepUR  ``l\_index  eqof``  0
  THEN  Unfold  `mu`  0)

---

Home Index