open import Agda.Builtin.Nat renaming (Nat to ℕ) hiding (_-_)
open import Agda.Builtin.List
open import Agda.Builtin.Equality

data ⊥ : Set where

infix 3 ¬_
¬_ : (A : Set) → Set
¬ A = A → ⊥

⊥-elim : {A : Set} → ⊥ → A
⊥-elim ()

data Dec (A : Set) : Set where
  yes :   A → Dec A
  no  : ¬ A → Dec A

natEq : (n m : ℕ) → Dec (n ≡ m)
natEq zero zero = yes refl
natEq zero (suc m) = no (λ ())
natEq (suc n) zero = no (λ ())
natEq (suc n) (suc m) with natEq n m
...                   | yes refl = yes refl
...                   | no  neq  = no φ
                                   where φ : _
                                         φ refl = neq refl

infixl 3 _-_
_-_ : List ℕ → ℕ → List ℕ
[] - x = []
x ∷ xs - y with natEq x y
.y ∷ xs - y | yes refl = xs - y
x  ∷ xs - y | no  _    = x ∷ (xs - y)


data Foo : List ℕ → Set where
  create : Foo (0 ∷ [])
  delete : {xs : List ℕ} → (y : ℕ) → Foo xs → Foo (xs - y)

foo[] : Foo []
foo[] = delete zero create

data Bar : List ℕ → Set where
  create : (x : ℕ) → Bar (x ∷ [])
  delete : {xs : List ℕ} → (y : ℕ) → Bar xs → Bar (xs - y)

bar[] : Bar []
bar[] = delete zero (create zero)

data Baz : ℕ → List ℕ → Set where
  create : (x : ℕ) → Baz x (x ∷ [])
  delete : {x : ℕ} {xs : List ℕ} → (y : ℕ) → Baz x xs → Baz x (xs - y)

baz[] : (x : ℕ) → Baz x []
baz[] x = lemma x (x ∷ [] - x) [] (delete x (create x)) (inv x)
  where
    inv : (x : ℕ) → (x ∷ [] - x) ≡ []
    inv x with natEq x x
    inv x | yes refl = refl
    inv x | no x₁ = ⊥-elim (x₁ refl)
    lemma : ∀ x xs ys → Baz x xs → xs ≡ ys → Baz x ys
    lemma x₁ xs .xs x₂ refl = x₂