module Finite where

open import Relation.Binary.PropositionalEquality
open import Data.Empty

data _-_ (A : Set)(a : A) : Set where
  el : (b : A) → (a ≡ b → ⊥) → A - a

data IsFin : Set → Set where
  empty : IsFin ⊥
  suc : ∀ {A} (a : A) → IsFin (A - a) → IsFin A

data Noeth : Set → Set where
  noeth : ∀ {A} → ((a : A) → Noeth (A - a)) → Noeth A