| lapply linear track_inv_scut to H3; decompose; destruct;
lapply linear track_inv_impw to H4; decompose; destruct;
lapply linear track_inv_impr to H5; decompose; destruct; autobatch
| lapply linear track_inv_scut to H3; decompose; destruct;
lapply linear track_inv_impw to H4; decompose; destruct;
lapply linear track_inv_impr to H5; decompose; destruct; autobatch