imp_r.
repeattac (andM_l 1).
orA_r2.
andM_r (3::nil).
init.
andM_r (2::nil).
then orA_r1 init.
then orA_r2 init.