Introduce theorems on len of init and tail
Introduce mid function

mid computes the middle element of even length chains