-[ elim (eq_bind2_dec I1 I2) #HI
- [ elim (eq_term_dec V1 V2) #HV /2 width=1 by or_introl/ ]
- @or_intror #H destruct /2 width=1 by/
-| @or_intror #H destruct
-| @or_intror #H destruct
-| elim (eq_bind1_dec I1 I2) #HI /2 width=1 by or_introl/
- @or_intror #H destruct /2 width=1 by/
+[1: elim (eq_bind2_dec I1 I2) #HI
+ [ elim (eq_term_dec V1 V2) #HV ]
+|4: elim (eq_bind1_dec I1 I2) #HI