X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Flprs_tc.ma;h=b0602eaa0df48caf79620ec076284a61574d3981;hb=bd53c4e895203eb049e75434f638f26b5a161a2b;hp=cec8e47f5c1f75570f5e1fa008c9c9383c55988d;hpb=cac0166656e08399eaaf1a1e19f0ccea28c36d39;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 cec8e47f5..b0602eaa0 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
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/relocation/lex_tc.ma".
+include "static_2/relocation/lex_tc.ma".
 include "basic_2/rt_computation/lprs_ctc.ma".
 include "basic_2/rt_computation/cprs_lpr.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] 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] L2 → TC … (lex (λL.cpm h G L 0)) L1 L2.
 /3 width=3 by lprs_inv_CTC, lex_inv_CTC/ qed-.