theorem bior2a (a b: wff): $ (b -> a) -> (a \/ b <-> a) $;
a \/ b <-> b \/ a
(b -> a) -> (b \/ a <-> a)
(b -> a) -> (a \/ b <-> a)