:type let f : (a -> a) -> a -> a = \g. (\x. g (g x)) in f (\x. x+x)
:type let f : (a -> a) -> a -> a = \g. (\x. g (g x)) in f (\x. x-x)
:type let f : (a -> a) -> a -> a = \g. (\x. g (g x)) in f (\x. x/x)
:type let f : (a -> a) -> a -> a = \g. (\x. g (g x)) in f (\x. -x/x)
:type \x.x
:type \x. \y. x
:type \x. \y. \z. x + y + z
:type \x. \(y:Nat). x - y
:type \w. \x:Nat. \y. \z : Frac. w - x + y + z
\x. \y:Bool. x - y