| lapply linear track_inv_scut to H4; decompose; destruct;
lapply linear track_inv_lref to H5; decompose; autobatch
| lapply linear track_inv_scut to H3; decompose; destruct;
- lapply linear track_inv_prin to H5; destruct; autobatch
+ lapply linear track_inv_prin to H5; destruct;
+ lapply linear rinj_inj to Hcut1;
+ rewrite < Hcut1 in H4; clear Hcut1 a2;
+ autobatch
| lapply linear track_inv_scut to H3; decompose; destruct;
lapply linear track_inv_prin to H4; destruct; autobatch
| lapply linear track_inv_scut to H3; decompose; destruct;