elim (sta_inv_lift1 … HU2 … H … HVU) -H -U /3 width=8 by lstasa_ldec/
| #a #I #G #L #V #T1 #U1 #l #_ #IHTU1 #X #H
elim (sta_inv_bind1 … H) -H #U #HU1 #H destruct /3 width=1 by lstasa_bind/
elim (sta_inv_lift1 … HU2 … H … HVU) -H -U /3 width=8 by lstasa_ldec/
| #a #I #G #L #V #T1 #U1 #l #_ #IHTU1 #X #H
elim (sta_inv_bind1 … H) -H #U #HU1 #H destruct /3 width=1 by lstasa_bind/