Step * of Lemma swap_length

[T:Type]. ∀[L:T List]. ∀[i,j:ℕ||L||].  (||swap(L;i;j)|| ||L|| ∈ ℤ)
BY
(Unfold `swap` 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