-#L1 elim L1 -L1 [| #L1 #I1 #V1 #IHL1 ] * [2,4: #L2 #I2 #V2 ]
-[1,4: @or_intror #H destruct
-| elim (eq_bind2_dec I1 I2) #HI
- [ elim (eq_term_dec V1 V2) #HV
- [ elim (IHL1 L2) -IHL1 /2 width=1 by or_introl/ #HL ]
- ]
- @or_intror #H destruct /2 width=1 by/
-| /2 width=1 by or_introl/
+#L1 elim L1 -L1 [| #L1 #I1 #IHL1 ] * [2,4: #L2 #I2 ]
+[3: /2 width=1 by or_introl/
+|2: elim (eq_bind_dec I1 I2) #HI
+ [ elim (IHL1 L2) -IHL1 #HL /2 width=1 by or_introl/ ]