------------------------------------------------------------------------ -- The Agda standard library -- -- This module is DEPRECATED. Please use -- Data.List.Relation.Binary.Permutation.Inductive directly. ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} module Data.List.Relation.Permutation.Inductive where open import Data.List.Relation.Binary.Permutation.Inductive public