elim (ssta_inv_bind1 … H) -H #U2 #HTU2 #H destruct
elim (IHTU1 … HTU2) -T /3 width=1/
| #L #V #T #U1 #l1 #_ #IHTU1 #X #l2 #H
elim (ssta_inv_appl1 … H) -H #U2 #HTU2 #H destruct
elim (IHTU1 … HTU2) -T /3 width=1/
elim (ssta_inv_bind1 … H) -H #U2 #HTU2 #H destruct
elim (IHTU1 … HTU2) -T /3 width=1/
| #L #V #T #U1 #l1 #_ #IHTU1 #X #l2 #H
elim (ssta_inv_appl1 … H) -H #U2 #HTU2 #H destruct
elim (IHTU1 … HTU2) -T /3 width=1/