theorem eim (a b c: wff): $ a -> (b -> c) -> (a -> b) -> c $;
a -> (a -> b) -> b
a -> (b -> c) -> (a -> b) -> c