churchIncrement : ((a -> a) -> (a -> a)) -> ((a -> a) -> (a -> a))
churchIncrement n = \f => \x => n f (f x)

churchNumeral : Nat -> (a -> a) -> (a -> a)
churchNumeral Z = \f => \x => x
churchNumeral (S k) = churchIncrement (churchNumeral k)

churchPlus : ((a -> a) -> (a -> a)) -> ((a -> a) -> (a -> a)) -> ((a -> a) -> (a -> a))
churchPlus m n = \f => \x => m f (n f x)

churchMultiply : ((a -> a) -> (a -> a)) -> ((a -> a) -> (a -> a)) -> ((a -> a) -> (a -> a))
churchMultiply m n = \f => \x => m (n f) x

churchPow : ((a -> a) -> (a -> a)) -> (((a -> a) -> (a -> a)) -> ((a -> a) -> (a -> a))) -> ((a -> a) -> (a -> a))
churchPow m n = \f => \x => (n m) f x

c : Nat
c = 4

f : Integer -> Integer