Commit 2021-10-26 22:41 b5925894
View on Github →refactor(order/boolean_algebra): factor out pi.sdiff and pi.compl (#9955)
Provide definitional lemmas about sdiff and compl on pi types.
This allows usage later on even without a whole boolean_algebra instance.