[ #H1 #H2 destruct /2 width=4 by ex3_intro/
| #s #H1 #H2 #H3 #Hs destruct
elim (cpm_inv_sort1 … HX2) -HX2 #H #Hn2 destruct >iter_n_Sm
[ #H1 #H2 destruct /2 width=4 by ex3_intro/
| #s #H1 #H2 #H3 #Hs destruct
elim (cpm_inv_sort1 … HX2) -HX2 #H #Hn2 destruct >iter_n_Sm