| #L1 #H1 #V1 #IH * normalize
[ #T1 #T2 #_ <plus_n_Sm #H destruct
| #L2 #I2 #V2 #T1 #T2 #H1 #H2
- elim (IH … H1 ?) -IH -H1 /2 width=1/ -H2 #H1 #H2 destruct /2 width=1/
+ elim (IH … H1) -IH -H1 /2 width=1/ -H2 #H1 #H2 destruct /2 width=1/
]
]
qed-.
-
\ No newline at end of file