Inductive nat : Type :=
| O : nat
| S : nat -> nat.

Inductive list (A: Type) : Type :=
| nil: list A
| conc: A -> (list A) -> (list A).

Inductive listn (A: Type) : V (n: nat). Type :=
| niln: listn A O
| concn: V (a:A). V (n: nat). V (l: listn A n). listn A (S n).


Inductive nat : Type :=
| O : nat
| S : V (x: nat). nat.

Recursive plus (a: nat) (b: nat) [0]: nat :=
     match a with
       | b
       | \ (a: nat). S (plus a b).


Definition zero : nat :=
      plus O O.

Definition zero2 :=
      plus O O.

Definition zero3 (a: nat) (b: nat) : nat :=
      plus a b.

Definition zero4 (a: nat) (b: nat) := plus a b.

Extract Def.