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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx.ma
index ff62c4d6b..4503f5e3e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx.ma
@@ -29,13 +29,13 @@ interpretation
 
 (* Basic_2A1: uses: lsx_ind *)
 lemma rdsx_ind (h) (o) (G) (T):
-               ∀R:predicate lenv.
+               ∀Q:predicate lenv.
                (∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
-                     (∀L2. ⦃G, L1⦄ ⊢ ⬈[h] L2 → (L1 ≛[h, o, T] L2 → ⊥) → R L2) →
-                     R L1
+                     (∀L2. ⦃G, L1⦄ ⊢ ⬈[h] L2 → (L1 ≛[h, o, T] L2 → ⊥) → Q L2) →
+                     Q L1
                ) →
-               ∀L. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄ → R L.
-#h #o #G #T #R #H0 #L1 #H elim H -L1
+               ∀L. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄ →  Q L.
+#h #o #G #T #Q #H0 #L1 #H elim H -L1
 /5 width=1 by SN_intro/
 qed-.