theorem orim1 (a b c: wff): $ (a -> b) -> a \/ c -> b \/ c $;
(a -> b) -> a -> b
(a -> b) -> a \/ c -> b \/ c