- [ lapply lift_mono to H1, H2. clear H2. subst.
- lapply linear lift_inv_sort_1 to H1. subst.
- lapply linear lift_inv_sort_1 to H3. subst. autobatch
- | lapply lift_mono to H2, H3. clear H3. subst.
+ [ lapply lift_mono to H1, H2. clear H2. destruct.
+ lapply linear lift_inv_sort_1 to H1. destruct.
+ lapply linear lift_inv_sort_1 to H3. destruct. autobatch
+ | lapply lift_mono to H2, H3. clear H3. destruct.