X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Flifts_teqw.ma;h=d03e0ab401c119b636baa2c4bf5ac703908429d6;hp=532d0b2364ee4ebdf6f9559a0a22641c1ffd3f5b;hb=98e786e1a6bd7b621e37ba7cd4098d4a0a6f8278;hpb=5d9f7ae4bad2b5926f615141c12942b9a8eb23fb

diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqw.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqw.ma
index 532d0b236..d03e0ab40 100644
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqw.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqw.ma
@@ -69,7 +69,7 @@ lemma teqw_inv_lifts_bi: deliftable2_bi teqw.
 | #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
@@ -98,7 +98,7 @@ qed-.
 
 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/