elim (IHn … Hnl) -IHn
[ #H lapply (tstc_inv_atom1 … H) -H #H >H -H /2 width=1 by or_intror/
| generalize in match Hnl; -Hnl @(nat_ind_plus … n) -n
elim (IHn … Hnl) -IHn
[ #H lapply (tstc_inv_atom1 … H) -H #H >H -H /2 width=1 by or_intror/
| generalize in match Hnl; -Hnl @(nat_ind_plus … n) -n