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