---

Step * of Lemma list_update_length

∀[l:Top List]. ∀[i:ℤ]. ∀[x:Top].  (||l[i:=x]|| ~ ||l||)
BY
{ ((UnivCD THENA Auto) THEN Assert ⌜||l[i:=x]|| = ||l|| ∈ ℤ⌝⋅) }

1
.....assertion..... 
1. l : Top List
2. i : ℤ
3. x : Top
⊢ ||l[i:=x]|| = ||l|| ∈ ℤ

2
1. l : Top List
2. i : ℤ
3. x : Top
4. ||l[i:=x]|| = ||l|| ∈ ℤ
⊢ ||l[i:=x]|| ~ ||l||

---

Latex:

---

Latex:
\mforall{}[l:Top  List].  \mforall{}[i:\mBbbZ{}].  \mforall{}[x:Top].    (||l[i:=x]||  \msim{}  ||l||)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Assert  \mkleeneopen{}||l[i:=x]||  =  ||l||\mkleeneclose{}\mcdot{})

---

Home Index