Step
*
of Lemma
swap_select
No Annotations
∀[T:Type]. ∀[L:T List]. ∀[i,j,x:ℕ||L||]. (swap(L;i;j)[x] = L[(i, j) x] ∈ T)
BY
{ (((Auto THEN Unfold `swap` 0) THEN RWO "permute_list_select" 0) THEN Auto') }
Latex:
Latex:
No Annotations
\mforall{}[T:Type]. \mforall{}[L:T List]. \mforall{}[i,j,x:\mBbbN{}||L||]. (swap(L;i;j)[x] = L[(i, j) x])
By
Latex:
(((Auto THEN Unfold `swap` 0) THEN RWO "permute\_list\_select" 0) THEN Auto')
Home
Index