comm und assoc in Laws

Gehören Kommutativ- und Assoziativgesetze nicht auch eher in Laws.v statt IntroElim.v?

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information