Lists - done
Poly - done
MoreCoq - partially done
Poly - change def of split
MoreCoq - until split_combine
MoreCoq - done