-[ * normalize /2 width=1 by conj/
- #K2 #I2 #V2 #L1 #L2 #H1 #H2 destruct
- normalize in H2; >append_length in H2; #H
- elim (plus_xySz_x_false … H)
-| #K1 #I1 #V1 #IH * normalize
- [ #L1 #L2 #H1 #H2 destruct
- normalize in H2; >append_length in H2; #H
- elim (plus_xySz_x_false … (sym_eq … H))
- | #K2 #I2 #V2 #L1 #L2 #H1 #H2
- elim (destruct_lpair_lpair … H1) -H1 #H1 #H3 #H4 destruct (**) (* destruct lemma needed *)
+[ * /2 width=1 by conj/
+ #K2 #I2 #V2 #L1 #L2 >append_atom >append_pair #H destruct
+ >length_pair >append_length >plus_n_Sm
+ #H elim (plus_xSy_x_false … H)
+| #K1 #I1 #V1 #IH *
+ [ #L1 #L2 >append_pair >append_atom #H destruct
+ >length_pair >append_length >plus_n_Sm #H
+ lapply (discr_plus_x_xy … H) -H #H destruct
+ | #K2 #I2 #V2 #L1 #L2 >append_pair >append_pair #H1 #H2
+ elim (destruct_lpair_lpair_aux … H1) -H1 #H1 #H3 #H4 destruct (**) (* destruct lemma needed *)