Theorem normalize_idem

Modification history