[Refractor] contradiction over ⊥-elim in commutes-with-∪ def

[Refractor] contradiction over ⊥-elim in commutes-with-∪ def #4532