Agda-2.6.0: src/data/lib/prim/Agda/Builtin/Equality/Rewrite.agda
{-# OPTIONS --without-K --rewriting --no-sized-types --no-guardedness #-}
module Agda.Builtin.Equality.Rewrite where
open import Agda.Builtin.Equality
{-# BUILTIN REWRITE _≡_ #-}
{-# OPTIONS --without-K --rewriting --no-sized-types --no-guardedness #-}
module Agda.Builtin.Equality.Rewrite where
open import Agda.Builtin.Equality
{-# BUILTIN REWRITE _≡_ #-}