##[ ##1: #H1; napply (decidable_strid_aux1 … (neqstr_to_neq … H1))
##| ##2: #H1; napply (decidable_strid_aux2 … (neqnat_to_neq … H1))
##]
##[ ##1: #H1; napply (decidable_strid_aux1 … (neqstr_to_neq … H1))
##| ##2: #H1; napply (decidable_strid_aux2 … (neqnat_to_neq … H1))
##]