---

Step * 1 of Lemma l_index_hd


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
BY
{ (RecUnfold `mu-ge` 0 THEN Reduce 0 THEN (SplitOnConclITE THENA Auto) THEN Try (Trivial) THEN D -1 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  dT  :  EqDecider(T)
3.  u  :  T
4.  v  :  T  List
5.  \mneg{}False
\mvdash{}  mu-ge(\mlambda{}i.(dT  u  [u  /  v][i]);0)  \msim{}  0


By

---

Latex:
(RecUnfold  `mu-ge`  0
  THEN  Reduce  0
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  Try  (Trivial)
  THEN  D  -1
  THEN  Auto)

---

Home Index