elim (sta_inv_bind1 … H) -H #U2 #HTU2 #H destruct /3 width=1/
| #L #V #T #U1 #_ #IHTU1 #X #H
elim (sta_inv_appl1 … H) -H #U2 #HTU2 #H destruct /3 width=1/
elim (sta_inv_bind1 … H) -H #U2 #HTU2 #H destruct /3 width=1/
| #L #V #T #U1 #_ #IHTU1 #X #H
elim (sta_inv_appl1 … H) -H #U2 #HTU2 #H destruct /3 width=1/