Step
*
of Lemma
swap_length
∀[T:Type]. ∀[L:T List]. ∀[i,j:ℕ||L||].  (||swap(L;i;j)|| = ||L|| ∈ ℤ)
BY
{ (Unfold `swap` 0 THEN Auto) }
Latex:
Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[i,j:\mBbbN{}||L||].    (||swap(L;i;j)||  =  ||L||)
By
Latex:
(Unfold  `swap`  0  THEN  Auto)
Home
Index