Definition int := (A:Prop)(A->A)->A->A.

Definition O := [A:Prop][s:A->A][o:A]o.

Definition S := [n:int][A:Prop][s:A->A][o:A](s (n A s o)).

Definition Uno := [A:Prop][s:A->A][o:A](s o).

Definition Due := [A:Prop][s:A->A][o:A](s (s o)).

Definition Tre := [A:Prop][s:A->A][o:A](s (s (s o))).

Definition id := [A:Prop][x:A]x.

Definition id_Due := (id int Due).

Definition difficult := ((S Due) (int -> int) (id (int -> int)) (id int)).

Definition is_Zero := [n:int](n int [_:int]Uno O).

Definition couple := [A:Prop][x:A][y:A][z:A->A->A](z x y).

Definition Couple := [A:Prop](z:A->A->A)A.

Definition fst := [A:Prop][x:A][y:A]x.

Definition snd := [A:Prop][x:A][y:A]y.

Definition next : (Couple int) -> (Couple int) := [x:(Couple int)](couple int (x (snd int)) (S (x (snd int)))).

Definition pred := [n:int]((n (Couple int) next (couple int O O))(fst int)).

Definition test := (((pred Tre) (int -> int))(id (int->int)) (id int)).