Issue254.agda

module Issue254 where

data Unit : Set where
  * : Unit

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

data Vec : Nat → Set where
  cons : ∀ n → Vec (suc n)

remove : ∀ n → Nat → Vec (suc n) → Unit
remove n x (cons .n) with *
remove n x (cons .n) | * = {!!}