theorem exim1 {x: nat} (a: wff) (b: wff x): $ E. x (a -> b) -> a -> E. x b $;
a -> (a -> b) -> b
a -> E. x (a -> b) -> E. x b
E. x (a -> b) -> a -> E. x b