Theorem Iff.elim_right

Modification history