- [ lapply linear nplus_inv_zero_1 to H2. subst.
- lapply nplus_mono to H1, H3. subst. auto
- | lapply linear nplus_inv_succ_1 to H3. decompose. subst.
- lapply linear nplus_inv_succ_1 to H4. decompose. subst.
- lapply linear nplus_inv_succ_2 to H5. decompose. subst. auto
+ [ lapply linear nplus_inv_zero_1 to H2. destruct.
+ lapply nplus_mono to H1, H3. destruct. autobatch
+ | lapply linear nplus_inv_succ_1 to H3. decompose. destruct.
+ lapply linear nplus_inv_succ_1 to H4. decompose. destruct.
+ lapply linear nplus_inv_succ_2 to H5. decompose. destruct. autobatch