---

Step * 1 of Lemma int-list-index-append


1. x : ℤ
⊢ ∀[L2:ℤ List]
    (int-list-index(L2;x) ~ if int-list-member(x;[]) then int-list-index([];x) else 0 + int-list-index(L2;x) fi )
BY
{ TACTIC:AutoSplit }

---

Latex:

---

Latex:

1.  x  :  \mBbbZ{}
\mvdash{}  \mforall{}[L2:\mBbbZ{}  List]
        (int-list-index(L2;x)  \msim{}  if  int-list-member(x;[])
        then  int-list-index([];x)
        else  0  +  int-list-index(L2;x)
        fi  )


By

---

Latex:
TACTIC:AutoSplit

---

Home Index