- | lapply linear track_inv_scut to H3; decompose; subst;
- lapply linear track_inv_prin to H5; subst; autobatch
- | lapply linear track_inv_scut to H3; decompose; subst;
- lapply linear track_inv_prin to H4; subst; autobatch
- | lapply linear track_inv_scut to H3; decompose; subst;
- lapply linear track_inv_impw to H4; decompose; subst;
- lapply linear track_inv_impr to H5; decompose; subst; autobatch
+ | lapply linear track_inv_scut to H3; decompose; destruct;
+ lapply linear track_inv_prin to H5; destruct;
+ lapply linear rinj_inj to Hcut1; destruct; autobatch
+ | lapply linear track_inv_scut to H3; decompose; destruct;
+ lapply linear track_inv_prin to H4; destruct;
+ lapply linear linj_inj to Hcut; 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