Theorem Down.mem_compression_of_insert_mem_compression

Modification history