X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Flprs_tc.ma;h=cc3fadc33abe951766c66b0481ea232b1a5013fb;hb=2c9f4fddc259b09b6e71b18eef78f0bed38eeb14;hp=122051b4d7c4a97d679ba78055715374b5b1552c;hpb=ff612dc35167ec0c145864c9aa8ae5e1ebe20a48;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_tc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_tc.ma
index 122051b4d..cc3fadc33 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_tc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_tc.ma
@@ -21,11 +21,11 @@ include "basic_2/rt_computation/cprs_lpr.ma".
 (* Properties with transitive closure ***************************************)
 
 lemma lprs_TC (h) (G):
-              ∀L1,L2. TC … (lex (λL.cpm h G L 0)) L1 L2 → ⦃G, L1⦄⊢ ➡*[h] L2.
+              ∀L1,L2. TC … (lex (λL.cpm h G L 0)) L1 L2 → ❪G,L1❫⊢ ➡*[h,0] L2.
 /4 width=3 by lprs_CTC, lex_CTC, lpr_cprs_trans/ qed.
 
 (* Inversion lemmas with transitive closure *********************************)
 
 lemma lprs_inv_TC (h) (G):
-                  ∀L1,L2. ⦃G, L1⦄⊢ ➡*[h] L2 → TC … (lex (λL.cpm h G L 0)) L1 L2.
+                  ∀L1,L2. ❪G,L1❫⊢ ➡*[h,0] L2 → TC … (lex (λL.cpm h G L 0)) L1 L2.
 /3 width=3 by lprs_inv_CTC, lex_inv_CTC/ qed-.