renaming

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

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 827a963be43836ab25f59e72b583677b5c80d0b6..1ee9f365b2326256fcd60a148e7170ee56476568 100644 (file)
--- 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-.