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).

Recursive T (A: Type) (B: Type) (n: nat) [2] : Type :=
   match n with
     | A
     | \ (n: nat). (V (b: B). T A B n).

Compute (T nat nat (S (S O))).

Recursive fold2 (A: Type) (B: Type) (f: V (a: A). V (b: B). A) (n: nat) (b: B) [3] : V (H: T A B n). T A B n :=
     match n with
       | \ (x: A). f x b
       | \ (n: nat).
                \ (g: T A B (S n)). \ (y2: B). 
                          fold2 A B f n b (g y2).

Recursive fold (A: Type) (B: Type) (f: V (a: A). V (b: B). A) (a: A) (n: nat) [4] : T A B n :=
     match n with
       | a
       | \ (n: nat). \ (x: B). fold2 A B f n x (fold A B f a n).

Check (fold nat nat plus O).

Definition sum : V (n: nat). T nat nat n :=
     fold nat nat plus O.

Check (sum).

Check (sum (S (S (S O)))).

Check (sum (S (S (S O))) (S (S (S O)))).

Check (sum (S (S (S O))) (S (S (S O))) (S (S (S O)))).

Check (sum (S (S (S O))) (S (S (S O))) (S (S (S O))) (S (S (S O)))).

Compute (sum (S (S (S O))) (S (S (S O))) (S (S (S O))) (S (S (S O)))).

Compute (plus (S (S (S O))) (S (S (S O)))).