lapply (transitive_le … Hde2d1 Hdi1) -Hde2d1 #Hde2i1
lapply (tps_weak … HWT2 0 (i1 + 1) ? ?) -HWT2 normalize /2 width=1/ -Hde2i1 #HWT2
<(tps_inv_lift1_eq … HWT2 … HVW) -HWT2 /4 width=4/
lapply (transitive_le … Hde2d1 Hdi1) -Hde2d1 #Hde2i1
lapply (tps_weak … HWT2 0 (i1 + 1) ? ?) -HWT2 normalize /2 width=1/ -Hde2i1 #HWT2
<(tps_inv_lift1_eq … HWT2 … HVW) -HWT2 /4 width=4/