X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Flpxs.ma;h=61fa33126cb50c723edbe4a4171ad1e79e07739f;hp=9375fee8d33661dbee357b5fd39e911757a80ed1;hb=5c186c72f508da0849058afeecc6877cd9ed6303;hpb=282511a928532676813d99d08594cd5f98fcb80e

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma
index 9375fee8d..61fa33126 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma
@@ -67,15 +67,15 @@ lemma lpxs_inv_pair_dx (h) (G): ∀I,L1,K2,V2. ⦃G, L1⦄ ⊢ ⬈*[h] K2.ⓑ{I}
 (* Basic eliminators ********************************************************)
 
 (* Basic_2A1: was: lpxs_ind_alt *)
-lemma lpxs_ind (h) (G): ∀R:relation lenv.
-                        R (⋆) (⋆) → (
+lemma lpxs_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-.