fun rot 0 L = L
  | rot N nil = nil
  | rot N (H :: T) = rot (N - 1) (T @ H :: [])


fun length nil = 0
  | length (H :: T) = 1 + (length T)




To show:

  * rot (length L) L = L


From class: 

   L1 @ nil = L1
   @ is associative

Generalize induction hyp.

Lemma:  If N = length L1
        then rot N (L1 @ L2) = L2 @ L1
Proof:  case L1 = nil.
	  * length nil = 0
          * N = 0.
          * rot (0) L2 = L2 = L2 @ nil

        case L1 = h :: t.
	  * n = length (h :: t @ L2) = 1 + length (t @ L2) > 0
	  * rot n (h :: t @ L2) = rot (n-1) (t @ L2 @ h :: []) 
                  = rot (n-1) (t @ (L2 @ h :: []))
                  = (L2 @ h :: []) @ L1
	          = L2 @ (h :: [] @ L1)
	          = L2 @ (h :: L1)

Thm :  If N = length L then rot N L = L
Proof: take L1 = L and L2 = [],  the claim follows by lemma.