irrelevant-add-preserves-leq-converse
max-empty-contradiction
max-preserves-leq*
added WORLDS to all remaining theorems.