Theorem himp_ne_right

Modification history