atが書けないぴーーーーーーー

data Unit : Set0 where
  unit : Unit

data Nat : Set0 where
  zero : Nat
  succ : Nat -> Nat

data Bool : Set0 where
  true : Bool
  false : Bool

_+_ : Nat -> Nat -> Nat
zero + b = b
(succ a) + b = succ (a + b)

data Hold (T : Set0) : Set0 where
  hold : Nat -> T -> Hold T

Vec : Nat -> Set0
Vec zero = Unit
Vec (succ a) = Hold (Vec a)

vappend : (m n : Nat) -> Vec m -> Vec n -> Vec (m + n)
vappend zero b as bs = bs
vappend (succ a) b (hold elem as') bs = hold elem (vappend a b as' bs)

at : (m n : Nat) -> Vec n -> Nat -- m < n
???

at : (m n : Nat) -> Vec n -> Id Bool (m < n) true -> Nat的な事をしてただまぁこの形だとdot-patternとか出て来ちゃいそうなソレなので色々遠回りすると出来そうですね。

というか多分dot-patternとImplicit Parameterを使わないというなぞの縛りを設けるならば、Leibniz Equalityの方が良い筈。