theorem bibi2 (a b: wff): $ b -> (a <-> b <-> a) $;
a <-> b <-> (b <-> a)
b -> (b <-> a <-> a)
b -> (a <-> b <-> a)