∀V,U. +ⓓV.U ≅ T → ⇧*[f]T ≘ U → ⊥.
@(f_ind … tw) #n #IH #T #Hn #f #V #U #H1 #H2 destruct
elim (tweq_inv_abbr_pos_sn … H1) -H1 #X1 #X2 #HX2 #H destruct -V
∀V,U. +ⓓV.U ≅ T → ⇧*[f]T ≘ U → ⊥.
@(f_ind … tw) #n #IH #T #Hn #f #V #U #H1 #H2 destruct
elim (tweq_inv_abbr_pos_sn … H1) -H1 #X1 #X2 #HX2 #H destruct -V