partial commit in static_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / relocation / lifts_teqw.ma

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 532d0b2364ee4ebdf6f9559a0a22641c1ffd3f5b..d03e0ab401c119b636baa2c4bf5ac703908429d6 100644 (file)
--- 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/