{-# OPTIONS --without-K #-} module Explore.Subset where open import Relation.Binary.PropositionalEquality -- TODO