data N : Set 0 where
  | O : N
  | S : N -> N;

one   : N = S O;
two   : N = S (S O);
three : N = S two;

plus : N -> N -> N;

data Parity : N -> Set where
 | even : (n:N) -> (Parity (plus n n))
 | odd  : (n:N) -> (Parity (S (plus n n)));

data Vect : (A:Set 0) -> (n:N) -> Set 0 where
  | Nil  : (A:Set 0) -> (Vect A O)
  | Cons : (A:Set 0) -> (k:N) -> (a:A) -> (Vect A k) -> (Vect A (S k));

vtail : (A:Set 0) -> (k:N) -> (Vect A (S k)) -> (Vect A k);
vappend : (A:Set) -> (m:N) -> (n:N) -> (Vect A m) -> (Vect A n) -> (Vect A (plus m n));
vadd : (m:N) -> (Vect N m) -> (Vect N m) -> (Vect N m);

data Infer : Set 0 where
  | MkInf : (A : Set) -> A -> Infer;

data PClause : Set 0 where
  | MkP : (A : Set) -> A -> A -> PClause;

npar : (n:N) -> (p:Parity n) -> N;