Dear all,
just an observation. The facts
List.drop_Suc_conv_tl:
?i < length ?xs ⟹
?xs ! ?i # drop (Suc ?i) ?xs = drop ?i ?xs
List.nth_drop':
?i < length ?xs ⟹
?xs ! ?i # drop (Suc ?i) ?xs = drop ?i ?xs
are duplicates of each other.
cheers
chris