Inductive nat: Type := | O: nat | S: 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). 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). Definition sum : V (n: nat). T nat nat n := fold nat nat plus O. Simpl (sum (S (S (S O)))). Typecheck (sum (S (S (S O))) (S (S (S O))) (S (S (S O))) (S (S (S O)))). Simpl (sum (S (S (S O))) (S (S (S O))) (S (S (S O))) (S (S (S O)))).