{-# OPTIONS --rewriting #-} module EqualityRewriting where open import Agda.Builtin.Equality public {-# BUILTIN REWRITE _≡_ #-}