Theorem List.tail_append_singleton_of_ne_nil

Modification history