lapply insert_trans to H5, H7; clear H7; decompose;
lapply ntrack_weak to H3, H6; decompose;
lapply H to H3, H10, H5; clear H H10; lapply linear H1 to H3, H9, H5;
lapply insert_trans to H5, H7; clear H7; decompose;
lapply ntrack_weak to H3, H6; decompose;
lapply H to H3, H10, H5; clear H H10; lapply linear H1 to H3, H9, H5;