---

Step * of Lemma select-cons

∀[x,L:Top]. ∀[i:ℤ].  ([x / L][i] ~ if i ≤z 0 then x else L[i - 1] fi )
BY
{ (Auto THEN AutoSplit) }

1
1. x : Top
2. L : Top
3. i : ℤ
4. i ≤ 0
⊢ [x / L][i] ~ x

2
1. x : Top
2. L : Top
3. i : ℤ
4. ¬(i ≤ 0)
⊢ [x / L][i] ~ L[i - 1]

---

Latex:

---

Latex:
\mforall{}[x,L:Top].  \mforall{}[i:\mBbbZ{}].    ([x  /  L][i]  \msim{}  if  i  \mleq{}z  0  then  x  else  L[i  -  1]  fi  )


By

---

Latex:
(Auto  THEN  AutoSplit)

---

Home Index