-#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 /2 width=1 by conj/
-#K1 #K2 #n #_ * #H1 #H2 >length_bind /3 width=1 by minus_Sn_m, conj/
+#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2
+[ /2 width=1 by conj/
+| #I1 #I2 #K1 #K2 #_ #IH >length_bind >length_bind //
+]
+#K1 #K2 #n #_ * #H1 #H2 destruct
+>length_bind <nminus_succ_dx <nminus_succ_sn
+/2 width=1 by nle_eq_zero_minus, conj/