[ lapply linear nplus_inv_zero_2 to H1. subst
| lapply linear nplus_inv_succ_2 to H3. decompose. subst.
lapply linear nplus_inv_succ_2 to H4. decompose. subst
[ lapply linear nplus_inv_zero_2 to H1. subst
| lapply linear nplus_inv_succ_2 to H3. decompose. subst.
lapply linear nplus_inv_succ_2 to H4. decompose. subst