partial commit in static_2

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

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 0a6831c7211bc81078c195c651cc6adbb9842102..b45a9e7e8d80f9b74f34293b2a0dc087405013c3 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqo.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_teqo.ma
@@ -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