X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Ftr_pap_tls.ma;h=ef36b6f3388519015fcad8b8127c97b8bbfda9ad;hb=73cc0c523c5264f2883c25f6735be325e5cfd1da;hp=da8ea1519527fc2299f606b796ea0a4ae5b1496c;hpb=345b9054da93e11139d3dfe07f83e444e3022fc1;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_tls.ma
index da8ea1519..ef36b6f33 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_tls.ma
@@ -24,7 +24,7 @@ lemma tr_pap_plus (p1) (p2) (f):
 #p1 #p2 elim p2 -p2
 [ * #p #f //
 | #i #IH * #p #f
-  <pplus_succ_dx <tr_pap_succ <tr_pap_succ
+  <pplus_succ_dx <tr_cons_pap_succ <tr_cons_pap_succ
   <IH -IH >nsucc_inj //
 ]
 qed.