-#l @(nat_ind_plus … l) -l // #l #_ #Hkl
-lapply (H (⋆(next h k)) ?) -H /2 width=2 by cpx_st/ -L -l #H destruct -H -e0 (**) (* destruct does not remove some premises *)
-lapply (next_lt h k) >e1 -e1 #H elim (lt_refl_false … H)
+#d @(nat_ind_plus … d) -d // #d #_ #Hkd
+lapply (H (⋆(next h k)) ?) -H /2 width=2 by cpx_st/ -L -d #H
+lapply (destruct_tatom_tatom_aux … H) -H #H (**) (* destruct lemma needed *)
+lapply (destruct_sort_sort_aux … H) -H #H (**) (* destruct lemma needed *)
+lapply (next_lt h k) >H -H #H elim (lt_refl_false … H)