X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Flprs_tc.ma;h=3b031c6d50f6f0c72039284b290e01c7d588d5ef;hp=122051b4d7c4a97d679ba78055715374b5b1552c;hb=f308429a0fde273605a2330efc63268b4ac36c99;hpb=87f57ddc367303c33e19c83cd8989cd561f3185b

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..3b031c6d5 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] 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-.