Theorem Finmap.insert_toFinmap

Modification history