{-# OPTIONS --safe --without-K #-} open import Reduction.Base public open import Reduction.Properties public