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.ma;h=1ee9f365b2326256fcd60a148e7170ee56476568;hp=827a963be43836ab25f59e72b583677b5c80d0b6;hb=5c186c72f508da0849058afeecc6877cd9ed6303;hpb=282511a928532676813d99d08594cd5f98fcb80e

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs.ma
index 827a963be..1ee9f365b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs.ma
@@ -65,15 +65,15 @@ lemma lprs_inv_pair_dx (h) (G):
 (* Basic eliminators ********************************************************)
 
 (* Basic_2A1: was: lprs_ind_alt *)
-lemma lprs_ind (h) (G): ∀R:relation lenv.
-                        R (⋆) (⋆) → (
+lemma lprs_ind (h) (G): ∀Q:relation lenv.
+                        Q (⋆) (⋆) → (
                           ∀I,K1,K2.
                           ⦃G, K1⦄ ⊢ ➡*[h] K2 →
-                          R K1 K2 → R (K1.ⓘ{I}) (K2.ⓘ{I})
+                          Q K1 K2 → Q (K1.ⓘ{I}) (K2.ⓘ{I})
                         ) → (
                           ∀I,K1,K2,V1,V2.
                           ⦃G, K1⦄ ⊢ ➡*[h] K2 → ⦃G, K1⦄ ⊢ V1 ➡*[h] V2 →
-                          R K1 K2 → R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2)
+                          Q K1 K2 → Q (K1.ⓑ{I}V1) (K2.ⓑ{I}V2)
                         ) →
-                        ∀L1,L2. ⦃G, L1⦄ ⊢ ➡*[h] L2 → R L1 L2.
+                        ∀L1,L2. ⦃G, L1⦄ ⊢ ➡*[h] L2 → Q L1 L2.
 /3 width=4 by lex_ind/ qed-.