update in ground

[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / tr_pap_tls.ma

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 978d360f6f20dcb038b5c9217c6558c97d35e02c..ef36b6f3388519015fcad8b8127c97b8bbfda9ad 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_tls.ma
@@ -19,12 +19,12 @@ include "ground/lib/stream_tls.ma".
 
 (* Constructions with stream_tls ********************************************)
 
-lemma tr_pap_plus (i1) (i2) (f):
-      (⇂*[ninj i2]f)@❨i1❩+f@❨i2❩ = f@❨i1+i2❩.
-#i1 #i2 elim i2 -i2
+lemma tr_pap_plus (p1) (p2) (f):
+      (⇂*[ninj p2]f)＠⧣❨p1❩+f＠⧣❨p2❩ = f＠⧣❨p1+p2❩.
+#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.