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_lpxs.ma;h=c9f49cfe19c41c5eaf0085dd4a3e6707f10b8cd2;hp=6f6676e9c368fcac422d3b56d7f17c34b832c491;hb=5c186c72f508da0849058afeecc6877cd9ed6303;hpb=282511a928532676813d99d08594cd5f98fcb80e

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_lpxs.ma
index 6f6676e9c..c9f49cfe1 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_lpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/rdsx_lpxs.ma
@@ -36,14 +36,14 @@ qed-.
 (* Eliminators with unbound rt-computation for full local environments ******)
 
 lemma rdsx_ind_lpxs_lfdeq (h) (o) (G):
-                          ∀T. ∀R:predicate lenv.
+                          ∀T. ∀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
                           ) →
                           ∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄  →
-                          ∀L0. ⦃G, L1⦄ ⊢ ⬈*[h] L0 → ∀L2. L0 ≛[h, o, T] L2 → R L2.
-#h #o #G #T #R #IH #L1 #H @(rdsx_ind … H) -L1
+                          ∀L0. ⦃G, L1⦄ ⊢ ⬈*[h] L0 → ∀L2. L0 ≛[h, o, T] L2 → Q L2.
+#h #o #G #T #Q #IH #L1 #H @(rdsx_ind … H) -L1
 #L1 #HL1 #IH1 #L0 #HL10 #L2 #HL02
 @IH -IH /3 width=3 by rdsx_lpxs_trans, rdsx_lfdeq_trans/ -HL1 #K2 #HLK2 #HnLK2
 lapply (lfdeq_lfdneq_trans … HL02 … HnLK2) -HnLK2 #H
@@ -62,13 +62,13 @@ qed-.
 
 (* Basic_2A1: uses: lsx_ind_alt *)
 lemma rdsx_ind_lpxs (h) (o) (G):
-                    ∀T. ∀R:predicate lenv.
+                    ∀T. ∀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 #IH #L #HL
+                    ∀L. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄  → Q L.
+#h #o #G #T #Q #IH #L #HL
 @(rdsx_ind_lpxs_lfdeq … IH … HL) -IH -HL // (**) (* full auto fails *)
 qed-.