renaming

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / rdsx.ma

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 ff62c4d6b94e511383ac1428fa215b9138b6fdd0..4503f5e3e9bc1eeb320a94ae27f33bc218297b0c 100644 (file)
--- 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-.