X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Flifts_teqo.ma;h=b45a9e7e8d80f9b74f34293b2a0dc087405013c3;hb=98e786e1a6bd7b621e37ba7cd4098d4a0a6f8278;hp=be94378433006db33182e900570d67ec2b752c22;hpb=f677b4ef7fa20f1ab36c5ee59598865d5c1b719b;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqo.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqo.ma
index be9437843..b45a9e7e8 100644
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqo.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqo.ma
@@ -21,7 +21,7 @@ include "static_2/relocation/lifts_lifts.ma".
 
 lemma teqo_lifts_sn: liftable2_sn teqo.
 #T1 #T2 #H elim H -T1 -T2 [||| * ]
-[ #s1 #s2 #f #X #H 
+[ #s1 #s2 #f #X #H
   >(lifts_inv_sort1 … H) -H
   /2 width=3 by teqo_sort, ex2_intro/
 | #i #f #X #H
@@ -59,7 +59,7 @@ lemma teqo_inv_lifts_bi: deliftable2_bi teqo.
 | #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 teqo_lref/
 | #l #f #X1 #H1 #X2 #H2
   >(lifts_inv_gref2 … H1) -H1 >(lifts_inv_gref2 … H2) -H2