| #j #f #X1 #H1 #X2 #H2
elim (lifts_inv_lref2 … H1) -H1 #i1 #Hj1 #H destruct
elim (lifts_inv_lref2 … H2) -H2 #i2 #Hj2 #H destruct
- <(at_inj … Hj2 … Hj1) -j -f -i1
+ <(pr_pat_inj … Hj2 … Hj1) -j -f -i1
/1 width=1 by teqw_lref/
| #l #f #X1 #H1 #X2 #H2
>(lifts_inv_gref2 … H1) -H1 >(lifts_inv_gref2 … H2) -H2
lemma teqw_inv_abbr_pos_x_lifts_y_y (T) (f):
∀V,U. +ⓓV.U ≃ T → ⇧*[f]T ≘ U → ⊥.
-@(f_ind … tw) #n #IH #T #Hn #f #V #U #H1 #H2 destruct
+@(wf1_ind_nlt … tw) #n #IH #T #Hn #f #V #U #H1 #H2 destruct
elim (teqw_inv_abbr_pos_sn … H1) -H1 #X1 #X2 #HX2 #H destruct -V
elim (lifts_inv_bind1 … H2) -H2 #Y1 #Y2 #_ #HXY2 #H destruct
/2 width=7 by/