[ elim (eq_bind2_dec I1 I2) /2 width=1 by or_introl/ #HI ]
@or_intror #H destruct /2 width=1 by/
| elim (eq_flat2_dec I1 I2) /2 width=1 by or_introl/ #HI
[ elim (eq_bind2_dec I1 I2) /2 width=1 by or_introl/ #HI ]
@or_intror #H destruct /2 width=1 by/
| elim (eq_flat2_dec I1 I2) /2 width=1 by or_introl/ #HI