Theorem himp_le_himp

Modification history