MoreCoq.v: complete through app_length_twice