{-# OPTIONS --without-K --rewriting --no-sized-types --no-guardedness --no-subtyping #-} module Agda.Builtin.Equality.Rewrite where open import Agda.Builtin.Equality {-# BUILTIN REWRITE _≡_ #-}