Theorem Function.insert_injOn

Modification history