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