data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero    + n = n
(suc n) + m = suc (n + m)

data _≡_ {A : Set}(x : A) : A → Set where
  refl : x ≡ x

data _≢_ : ℕ →  ℕ → Set where
  _<_ : (n m : ℕ) → n ≢ (n + (suc m))
  _>_ : (m n : ℕ) → (n + (suc m)) ≢ n

----------------------------------------

data List (A : Set) : Set where
  []   : List A
  _::_ : A → List A → List A

[_] : {A : Set} → A → List A
[ x ] = x :: []


data Project (a : ℕ) : List ℕ → List ℕ → Set where
  empty    : Project a [] []

  distinct : ∀{xs ys}
             → (n : ℕ)
             → Project a xs ys
             → a ≢ n
             → Project a (n :: xs) (n :: ys)

  same     : ∀{xs ys}
             → (n : ℕ)
             → Project a xs ys
             → a ≡ n
             → Project a (n :: xs) ys

----------------------------------------

data _⊎_ (A B : Set) : Set where
  left :  A → A ⊎ B
  right : B → A ⊎ B

extend : (n m : ℕ)
         → (n ≡ m) ⊎ (n ≢ m)
         → ((suc n) ≡ (suc m)) ⊎ ((suc n) ≢ (suc m))
extend n .n (left refl) = left refl
extend n .(n + suc m) (right (.n < m)) = right (suc n < m)
extend .(m + suc m₁) m (right (m₁ > .m)) = right (m₁ > suc m)

total : (n m : ℕ) → (n ≡ m) ⊎ (n ≢ m)
total zero zero = left refl
total zero (suc m) = right (zero < m)
total (suc n) zero = right (n > zero)
total (suc n) (suc m) = extend n m (total n m)

----------------------------------------


_∖_==_ : List ℕ → ℕ → List ℕ → Set
xs ∖ x == ys = Project x xs ys


noop : (x : ℕ) → [ x ] ∖ x == []
noop = λ x → same x empty refl


data Foo : List ℕ → Set where
  empty  : Foo []
  add    : ∀{xs} → (x : ℕ) → Foo xs → Foo (x :: xs)
  delete : ∀{xs ys}
           → (x : ℕ)
           → Foo xs
           → {_ : xs ∖ x == ys}
           → Foo ys

-- Agda can fill the holes with Auto(), but can't compute the proofs implicitly?

single : (n : ℕ) → Foo []
single n = delete n (add n empty) {noop n}

double : (n m : ℕ) → Foo []
double n m with (total m n)
...           | left  x = delete n (add n empty) {?}
...           | right x = delete n (delete m (add n (add m empty)) {?}) {?}