From 5c186c72f508da0849058afeecc6877cd9ed6303 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 23 Jun 2018 20:03:00 +0200
Subject: [PATCH] renaming

+ the predicate in elimination principles in now Q uniformly
---
 .../basic_2/i_static/tc_lfxs_fqup.ma          | 16 +++----
 .../contribs/lambdadelta/basic_2/names.txt    |  6 ++-
 .../basic_2/relocation/lexs_lexs.ma           |  2 +-
 .../basic_2/rt_computation/cpms.ma            |  4 +-
 .../basic_2/rt_computation/cprs.ma            | 20 ++++-----
 .../basic_2/rt_computation/cpxs.ma            | 16 +++----
 .../lambdadelta/basic_2/rt_computation/csx.ma | 10 ++---
 .../basic_2/rt_computation/csx_aaa.ma         | 28 ++++++------
 .../basic_2/rt_computation/csx_cpxs.ma        | 16 +++----
 .../basic_2/rt_computation/fpbs.ma            | 12 ++---
 .../lambdadelta/basic_2/rt_computation/fsb.ma | 10 ++---
 .../basic_2/rt_computation/fsb_aaa.ma         | 34 +++++++-------
 .../basic_2/rt_computation/fsb_csx.ma         | 16 +++----
 .../basic_2/rt_computation/fsb_fpbg.ma        | 20 ++++-----
 .../basic_2/rt_computation/lprs.ma            | 10 ++---
 .../basic_2/rt_computation/lprs_lpr.ma        | 12 ++---
 .../basic_2/rt_computation/lpxs.ma            | 10 ++---
 .../basic_2/rt_computation/lpxs_lpx.ma        | 12 ++---
 .../basic_2/rt_computation/rdsx.ma            | 10 ++---
 .../basic_2/rt_computation/rdsx_lpxs.ma       | 20 ++++-----
 .../basic_2/rt_equivalence/cpcs.ma            | 12 ++---
 .../lambdadelta/basic_2/rt_transition/cpm.ma  | 44 +++++++++----------
 .../lambdadelta/basic_2/rt_transition/cpr.ma  | 36 +++++++--------
 .../lambdadelta/basic_2/rt_transition/cpx.ma  | 42 +++++++++---------
 .../lambdadelta/basic_2/s_computation/fqup.ma | 20 ++++-----
 .../basic_2/s_computation/fqup_weight.ma      | 20 ++++-----
 .../lambdadelta/basic_2/s_computation/fqus.ma | 14 +++---
 .../basic_2/s_transition/fqu_weight.ma        | 10 ++---
 .../lambdadelta/basic_2/static/frees_fqup.ma  | 22 +++++-----
 .../lambdadelta/basic_2/static/lfxs.ma        |  2 +-
 .../lambdadelta/basic_2/static/lfxs_drops.ma  |  6 +--
 .../basic_2/syntax/append_length.ma           |  6 +--
 32 files changed, 260 insertions(+), 258 deletions(-)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_fqup.ma
index 8eaf23735..3392f1e1a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_fqup.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_fqup.ma
@@ -40,18 +40,18 @@ qed.
 (* Advanced eliminators *****************************************************)
 
 lemma tc_lfxs_ind_sn: ∀R. c_reflexive … R →
-                      ∀L1,T. ∀R0:predicate …. R0 L1 →
-                      (∀L,L2. L1 ⪤**[R, T] L → L ⪤*[R, T] L2 → R0 L → R0 L2) →
-                      ∀L2. L1 ⪤**[R, T] L2 → R0 L2.
-#R #HR #L1 #T #R0 #HL1 #IHL1 #L2 #HL12
+                      ∀L1,T. ∀Q:predicate …. Q L1 →
+                      (∀L,L2. L1 ⪤**[R, T] L → L ⪤*[R, T] L2 → Q L → Q L2) →
+                      ∀L2. L1 ⪤**[R, T] L2 → Q L2.
+#R #HR #L1 #T #Q #HL1 #IHL1 #L2 #HL12
 @(TC_star_ind … HL1 IHL1 … HL12) /2 width=1 by lfxs_refl/
 qed-.
 
 lemma tc_lfxs_ind_dx: ∀R. c_reflexive … R →
-                      ∀L2,T. ∀R0:predicate …. R0 L2 →
-                      (∀L1,L. L1 ⪤*[R, T] L → L ⪤**[R, T] L2 → R0 L → R0 L1) →
-                      ∀L1. L1 ⪤**[R, T] L2 → R0 L1.
-#R #HR #L2 #R0 #HL2 #IHL2 #L1 #HL12
+                      ∀L2,T. ∀Q:predicate …. Q L2 →
+                      (∀L1,L. L1 ⪤*[R, T] L → L ⪤**[R, T] L2 → Q L → Q L1) →
+                      ∀L1. L1 ⪤**[R, T] L2 → Q L1.
+#R #HR #L2 #Q #HL2 #IHL2 #L1 #HL12
 @(TC_star_ind_dx … HL2 IHL2 … HL12) /2 width=4 by lfxs_refl/
 qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/names.txt b/matita/matita/contribs/lambdadelta/basic_2/names.txt
index 1f1d889d7..d80ea011a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/names.txt
+++ b/matita/matita/contribs/lambdadelta/basic_2/names.txt
@@ -9,8 +9,10 @@ IH     : reserved: inductive premise
 I,J    : item
 K,L    : local environment
 M,N    : reserved: future use
-O,P,Q  :
-R      : generic predicate (relation)
+O      :
+P      : relocation environment
+Q      : elimination predicate
+R      : generic predicate/relation
 S      : RTM stack
 T,U,V,W: term
 X,Y,Z  : reserved: transient objet denoted by a capital letter
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma
index 20e2f91a2..753b43b2e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma
@@ -51,7 +51,7 @@ theorem lexs_trans (RN) (RP) (f): (∀g,I,K. lexs_transitive RN RN RN RN RP g K
 /2 width=9 by lexs_trans_gen/ qed-.
 
 theorem lexs_trans_id_cfull: ∀R1,R2,R3,L1,L,f. L1 ⪤*[R1, cfull, f] L → 𝐈⦃f⦄ →
-                             ∀L2.  L ⪤*[R2, cfull, f] L2 → L1 ⪤*[R3, cfull, f] L2.
+                             ∀L2. L ⪤*[R2, cfull, f] L2 → L1 ⪤*[R3, cfull, f] L2.
 #R1 #R2 #R3 #L1 #L #f #H elim H -L1 -L -f
 [ #f #Hf #L2 #H >(lexs_inv_atom1 … H) -L2 // ]
 #f #I1 #I #K1 #K #HK1 #_ #IH #Hf #L2 #H
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms.ma
index 8d27710bd..2846c7536 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms.ma
@@ -37,14 +37,14 @@ lemma cpms_ind_sn (h) (G) (L) (T2) (Q:relation2 …):
                   Q 0 T2 →
                   (∀n1,n2,T1,T. ⦃G, L⦄ ⊢ T1 ➡[n1, h] T → ⦃G, L⦄ ⊢ T ➡*[n2, h] T2 → Q n2 T → Q (n1+n2) T1) →
                   ∀n,T1. ⦃G, L⦄ ⊢ T1 ➡*[n, h] T2 → Q n T1.
-#h #G #L #T2 #R @ltc_ind_sn_refl //
+#h #G #L #T2 #Q @ltc_ind_sn_refl //
 qed-.
 
 lemma cpms_ind_dx (h) (G) (L) (T1) (Q:relation2 …):
                   Q 0 T1 →
                   (∀n1,n2,T,T2. ⦃G, L⦄ ⊢ T1 ➡*[n1, h] T → Q n1 T → ⦃G, L⦄ ⊢ T ➡[n2, h] T2 → Q (n1+n2) T2) →
                   ∀n,T2. ⦃G, L⦄ ⊢ T1 ➡*[n, h] T2 → Q n T2.
-#h #G #L #T1 #R @ltc_ind_dx_refl //
+#h #G #L #T1 #Q @ltc_ind_dx_refl //
 qed-.
 
 (* Basic inversion lemmas ***************************************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs.ma
index 36d7644e6..230160ac7 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs.ma
@@ -20,11 +20,11 @@ include "basic_2/rt_computation/cpms.ma".
 (* Basic eliminators ********************************************************)
 
 (* Basic_2A1: was: cprs_ind_dx *)
-lemma cprs_ind_sn (h) (G) (L) (T2) (R:predicate …):
-                  R T2 →
-                  (∀T1,T. ⦃G, L⦄ ⊢ T1 ➡[h] T → ⦃G, L⦄ ⊢ T ➡*[h] T2 → R T → R T1) →
-                  ∀T1. ⦃G, L⦄ ⊢ T1 ➡*[h] T2 → R T1.
-#h #G #L #T2 #R #IH1 #IH2 #T1
+lemma cprs_ind_sn (h) (G) (L) (T2) (Q:predicate …):
+                  Q T2 →
+                  (∀T1,T. ⦃G, L⦄ ⊢ T1 ➡[h] T → ⦃G, L⦄ ⊢ T ➡*[h] T2 → Q T → Q T1) →
+                  ∀T1. ⦃G, L⦄ ⊢ T1 ➡*[h] T2 → Q T1.
+#h #G #L #T2 #Q #IH1 #IH2 #T1
 @(insert_eq_0 … 0) #n #H
 @(cpms_ind_sn … H) -n -T1 //
 #n1 #n2 #T1 #T #HT1 #HT2 #IH #H
@@ -33,11 +33,11 @@ elim (plus_inv_O3 n1 n2) // -H #H1 #H2 destruct
 qed-.
 
 (* Basic_2A1: was: cprs_ind *)
-lemma cprs_ind_dx (h) (G) (L) (T1) (R:predicate …):
-                  R T1 →
-                  (∀T,T2. ⦃G, L⦄ ⊢ T1 ➡*[h] T → ⦃G, L⦄ ⊢ T ➡[h] T2 → R T → R T2) →
-                  ∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h] T2 → R T2.
-#h #G #L #T1 #R #IH1 #IH2 #T2
+lemma cprs_ind_dx (h) (G) (L) (T1) (Q:predicate …):
+                  Q T1 →
+                  (∀T,T2. ⦃G, L⦄ ⊢ T1 ➡*[h] T → ⦃G, L⦄ ⊢ T ➡[h] T2 → Q T → Q T2) →
+                  ∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h] T2 → Q T2.
+#h #G #L #T1 #Q #IH1 #IH2 #T2
 @(insert_eq_0 … 0) #n #H
 @(cpms_ind_dx … H) -n -T2 //
 #n1 #n2 #T #T2 #HT1 #IH #HT2 #H
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma
index 88924f4e0..5b7495bd4 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma
@@ -26,17 +26,17 @@ interpretation "unbound context-sensitive parallel rt-computation (term)"
 
 (* Basic eliminators ********************************************************)
 
-lemma cpxs_ind: ∀h,G,L,T1. ∀R:predicate term. R T1 →
-                (∀T,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T → ⦃G, L⦄ ⊢ T ⬈[h] T2 → R T → R T2) →
-                ∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → R T2.
-#h #L #G #T1 #R #HT1 #IHT1 #T2 #HT12
+lemma cpxs_ind: ∀h,G,L,T1. ∀Q:predicate term. Q T1 →
+                (∀T,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T → ⦃G, L⦄ ⊢ T ⬈[h] T2 → Q T → Q T2) →
+                ∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → Q T2.
+#h #L #G #T1 #Q #HT1 #IHT1 #T2 #HT12
 @(TC_star_ind … HT1 IHT1 … HT12) //
 qed-.
 
-lemma cpxs_ind_dx: ∀h,G,L,T2. ∀R:predicate term. R T2 →
-                   (∀T1,T. ⦃G, L⦄ ⊢ T1 ⬈[h] T → ⦃G, L⦄ ⊢ T ⬈*[h] T2 → R T → R T1) →
-                   ∀T1. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → R T1.
-#h #G #L #T2 #R #HT2 #IHT2 #T1 #HT12
+lemma cpxs_ind_dx: ∀h,G,L,T2. ∀Q:predicate term. Q T2 →
+                   (∀T1,T. ⦃G, L⦄ ⊢ T1 ⬈[h] T → ⦃G, L⦄ ⊢ T ⬈*[h] T2 → Q T → Q T1) →
+                   ∀T1. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → Q T1.
+#h #G #L #T2 #Q #HT2 #IHT2 #T1 #HT12
 @(TC_star_ind_dx … HT2 IHT2 … HT12) //
 qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma
index 5e255d297..da0bbe1ee 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma
@@ -27,13 +27,13 @@ interpretation
 
 (* Basic eliminators ********************************************************)
 
-lemma csx_ind: ∀h,o,G,L. ∀R:predicate term.
+lemma csx_ind: ∀h,o,G,L. ∀Q:predicate term.
                (∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ →
-                     (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≛[h, o] T2 → ⊥) → R T2) →
-                     R T1
+                     (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≛[h, o] T2 → ⊥) → Q T2) →
+                     Q T1
                ) →
-               ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → R T.
-#h #o #G #L #R #H0 #T1 #H elim H -T1
+               ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ →  Q T.
+#h #o #G #L #Q #H0 #T1 #H elim H -T1
 /5 width=1 by SN_intro/
 qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_aaa.ma
index 722e8d8b6..4d54a74a5 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_aaa.ma
@@ -28,33 +28,33 @@ qed.
 
 (* Advanced eliminators *****************************************************)
 
-fact aaa_ind_csx_aux: ∀h,o,G,L,A. ∀R:predicate term.
+fact aaa_ind_csx_aux: ∀h,o,G,L,A. ∀Q:predicate term.
                       (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A →
-                            (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≛[h, o] T2 → ⊥) → R T2) → R T1
+                            (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≛[h, o] T2 → ⊥) → Q T2) → Q T1
                       ) →
-                      ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ T ⁝ A → R T.
-#h #o #G #L #A #R #IH #T #H @(csx_ind … H) -T /4 width=5 by cpx_aaa_conf/
+                      ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ T ⁝ A →  Q T.
+#h #o #G #L #A #Q #IH #T #H @(csx_ind … H) -T /4 width=5 by cpx_aaa_conf/
 qed-.
 
-lemma aaa_ind_csx: ∀h,o,G,L,A. ∀R:predicate term.
+lemma aaa_ind_csx: ∀h,o,G,L,A. ∀Q:predicate term.
                    (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A →
-                         (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≛[h, o] T2 → ⊥) → R T2) → R T1
+                         (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≛[h, o] T2 → ⊥) → Q T2) → Q T1
                    ) →
-                   ∀T. ⦃G, L⦄ ⊢ T ⁝ A → R T.
+                   ∀T. ⦃G, L⦄ ⊢ T ⁝ A → Q T.
 /5 width=9 by aaa_ind_csx_aux, aaa_csx/ qed-.
 
-fact aaa_ind_csx_cpxs_aux: ∀h,o,G,L,A. ∀R:predicate term.
+fact aaa_ind_csx_cpxs_aux: ∀h,o,G,L,A. ∀Q:predicate term.
                            (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A →
-                                 (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≛[h, o] T2 → ⊥) → R T2) → R T1
+                                 (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≛[h, o] T2 → ⊥) → Q T2) → Q T1
                            ) →
-                           ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ T ⁝ A → R T.
-#h #o #G #L #A #R #IH #T #H @(csx_ind_cpxs … H) -T /4 width=5 by cpxs_aaa_conf/
+                           ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ T ⁝ A →  Q T.
+#h #o #G #L #A #Q #IH #T #H @(csx_ind_cpxs … H) -T /4 width=5 by cpxs_aaa_conf/
 qed-.
 
 (* Basic_2A1: was: aaa_ind_csx_alt *)
-lemma aaa_ind_csx_cpxs: ∀h,o,G,L,A. ∀R:predicate term.
+lemma aaa_ind_csx_cpxs: ∀h,o,G,L,A. ∀Q:predicate term.
                         (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A →
-                              (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≛[h, o] T2 → ⊥) → R T2) → R T1
+                              (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≛[h, o] T2 → ⊥) → Q T2) → Q T1
                         ) →
-                        ∀T. ⦃G, L⦄ ⊢ T ⁝ A → R T.
+                        ∀T. ⦃G, L⦄ ⊢ T ⁝ A → Q T.
 /5 width=9 by aaa_ind_csx_cpxs_aux, aaa_csx/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma
index cfc4d6314..3a8a70ef9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma
@@ -35,13 +35,13 @@ qed-.
 
 (* Eliminators with unbound context-sensitive rt-computation for terms ******)
 
-lemma csx_ind_cpxs_tdeq: ∀h,o,G,L. ∀R:predicate term.
+lemma csx_ind_cpxs_tdeq: ∀h,o,G,L. ∀Q:predicate term.
                          (∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ →
-                               (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≛[h, o] T2 → ⊥) → R T2) → R T1
+                               (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≛[h, o] T2 → ⊥) → Q T2) → Q T1
                          ) →
                          ∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ →
-                         ∀T0. ⦃G, L⦄ ⊢ T1 ⬈*[h] T0 → ∀T2. T0 ≛[h, o] T2 → R T2.
-#h #o #G #L #R #IH #T1 #H @(csx_ind … H) -T1
+                         ∀T0. ⦃G, L⦄ ⊢ T1 ⬈*[h] T0 → ∀T2. T0 ≛[h, o] T2 → Q T2.
+#h #o #G #L #Q #IH #T1 #H @(csx_ind … H) -T1
 #T1 #HT1 #IH1 #T0 #HT10 #T2 #HT02
 @IH -IH /3 width=3 by csx_cpxs_trans, csx_tdeq_trans/ -HT1 #V2 #HTV2 #HnTV2
 lapply (tdeq_tdneq_trans … HT02 … HnTV2) -HnTV2 #H
@@ -59,11 +59,11 @@ elim (tdeq_dec h o T1 T0) #H
 qed-.
 
 (* Basic_2A1: was: csx_ind_alt *)
-lemma csx_ind_cpxs: ∀h,o,G,L. ∀R:predicate term.
+lemma csx_ind_cpxs: ∀h,o,G,L. ∀Q:predicate term.
                     (∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ →
-                          (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≛[h, o] T2 → ⊥) → R T2) → R T1
+                          (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≛[h, o] T2 → ⊥) → Q T2) → Q T1
                     ) →
-                    ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → R T.
-#h #o #G #L #R #IH #T #HT
+                    ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ →  Q T.
+#h #o #G #L #Q #IH #T #HT
 @(csx_ind_cpxs_tdeq … IH … HT) -IH -HT // (**) (* full auto fails *)
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma
index 78c6b2ef7..af6ca54c9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma
@@ -26,14 +26,14 @@ interpretation "parallel rst-computation (closure)"
 
 (* Basic eliminators ********************************************************)
 
-lemma fpbs_ind: ∀h,o,G1,L1,T1. ∀R:relation3 genv lenv term. R G1 L1 T1 →
-                (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≽[h, o] ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) →
-                ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2.
+lemma fpbs_ind: ∀h,o,G1,L1,T1. ∀Q:relation3 genv lenv term. Q G1 L1 T1 →
+                (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≽[h, o] ⦃G2, L2, T2⦄ → Q G L T → Q G2 L2 T2) →
+                ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → Q G2 L2 T2.
 /3 width=8 by tri_TC_star_ind/ qed-.
 
-lemma fpbs_ind_dx: ∀h,o,G2,L2,T2. ∀R:relation3 genv lenv term. R G2 L2 T2 →
-                   (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≽[h, o] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≥[h, o] ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) →
-                   ∀G1,L1,T1. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → R G1 L1 T1.
+lemma fpbs_ind_dx: ∀h,o,G2,L2,T2. ∀Q:relation3 genv lenv term. Q G2 L2 T2 →
+                   (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≽[h, o] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≥[h, o] ⦃G2, L2, T2⦄ → Q G L T → Q G1 L1 T1) →
+                   ∀G1,L1,T1. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → Q G1 L1 T1.
 /3 width=8 by tri_TC_star_ind_dx/ qed-.
 
 (* Basic properties *********************************************************)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb.ma
index 62fd4fe10..8ae6b26e8 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb.ma
@@ -31,13 +31,13 @@ interpretation
 
 (* Note: eliminator with shorter ground hypothesis *)
 (* Note: to be named fsb_ind when fsb becomes a definition like csx, lfsx ***)
-lemma fsb_ind_alt: ∀h,o. ∀R: relation3 …. (
+lemma fsb_ind_alt: ∀h,o. ∀Q: relation3 …. (
                       ∀G1,L1,T1. ≥[h,o] 𝐒⦃G1, L1, T1⦄ → (
-                         ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2
-                      ) → R G1 L1 T1
+                         ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ → Q G2 L2 T2
+                      ) → Q G1 L1 T1
                    ) →
-                   ∀G,L,T. ≥[h, o] 𝐒⦃G, L, T⦄ → R G L T.
-#h #o #R #IH #G #L #T #H elim H -G -L -T
+                   ∀G,L,T. ≥[h, o] 𝐒⦃G, L, T⦄ →  Q G L T.
+#h #o #Q #IH #G #L #T #H elim H -G -L -T
 /4 width=1 by fsb_intro/
 qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_aaa.ma
index 5b27cd1a9..43eb814dc 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_aaa.ma
@@ -27,42 +27,42 @@ theorem aaa_fsb: ∀h,o,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ≥[h, o] 𝐒⦃G,
 
 (* Advanced eliminators with atomic arity assignment for terms **************)
 
-fact aaa_ind_fpb_aux: ∀h,o. ∀R:relation3 ….
+fact aaa_ind_fpb_aux: ∀h,o. ∀Q:relation3 ….
                       (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A →
-                                    (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
-                                    R G1 L1 T1
+                                    (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ → Q G2 L2 T2) →
+                                    Q G1 L1 T1
                       ) →
-                      ∀G,L,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ∀A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T.
+                      ∀G,L,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ∀A. ⦃G, L⦄ ⊢ T ⁝ A →  Q G L T.
 #h #o #R #IH #G #L #T #H @(csx_ind_fpb … H) -G -L -T
 #G1 #L1 #T1 #H1 #IH1 #A1 #HTA1 @IH -IH //
 #G2 #L2 #T2 #H12 elim (fpbs_aaa_conf h o … G2 … L2 … T2 … HTA1) -A1
 /2 width=2 by fpb_fpbs/
 qed-.
 
-lemma aaa_ind_fpb: ∀h,o. ∀R:relation3 ….
+lemma aaa_ind_fpb: ∀h,o. ∀Q:relation3 ….
                    (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A →
-                                 (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
-                                 R G1 L1 T1
+                                 (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ → Q G2 L2 T2) →
+                                 Q G1 L1 T1
                    ) →
-                   ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T.
+                   ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → Q G L T.
 /4 width=4 by aaa_ind_fpb_aux, aaa_csx/ qed-.
 
-fact aaa_ind_fpbg_aux: ∀h,o. ∀R:relation3 ….
+fact aaa_ind_fpbg_aux: ∀h,o. ∀Q:relation3 ….
                        (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A →
-                                     (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
-                                     R G1 L1 T1
+                                     (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → Q G2 L2 T2) →
+                                     Q G1 L1 T1
                        ) →
-                       ∀G,L,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ∀A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T.
-#h #o #R #IH #G #L #T #H @(csx_ind_fpbg … H) -G -L -T
+                       ∀G,L,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ∀A. ⦃G, L⦄ ⊢ T ⁝ A →  Q G L T.
+#h #o #Q #IH #G #L #T #H @(csx_ind_fpbg … H) -G -L -T
 #G1 #L1 #T1 #H1 #IH1 #A1 #HTA1 @IH -IH //
 #G2 #L2 #T2 #H12 elim (fpbs_aaa_conf h o … G2 … L2 … T2 … HTA1) -A1
 /2 width=2 by fpbg_fwd_fpbs/
 qed-.
 
-lemma aaa_ind_fpbg: ∀h,o. ∀R:relation3 ….
+lemma aaa_ind_fpbg: ∀h,o. ∀Q:relation3 ….
                     (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A →
-                                  (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
-                                  R G1 L1 T1
+                                  (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → Q G2 L2 T2) →
+                                  Q G1 L1 T1
                     ) →
-                    ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T.
+                    ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → Q G L T.
 /4 width=4 by aaa_ind_fpbg_aux, aaa_csx/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma
index d1cc73d89..ffcbc3d80 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma
@@ -61,18 +61,18 @@ lemma csx_fsb: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ≥[h, o]
 
 (* Advanced eliminators *****************************************************)
 
-lemma csx_ind_fpb: ∀h,o. ∀R:relation3 genv lenv term.
+lemma csx_ind_fpb: ∀h,o. ∀Q:relation3 genv lenv term.
                    (∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ →
-                               (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
-                               R G1 L1 T1
+                               (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ → Q G2 L2 T2) →
+                               Q G1 L1 T1
                    ) →
-                   ∀G,L,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → R G L T.
+                   ∀G,L,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ →  Q G L T.
 /4 width=4 by fsb_inv_csx, csx_fsb, fsb_ind_alt/ qed-.
 
-lemma csx_ind_fpbg: ∀h,o. ∀R:relation3 genv lenv term.
+lemma csx_ind_fpbg: ∀h,o. ∀Q:relation3 genv lenv term.
                     (∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ →
-                                (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
-                                R G1 L1 T1
+                                (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → Q G2 L2 T2) →
+                                Q G1 L1 T1
                     ) →
-                    ∀G,L,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → R G L T.
+                    ∀G,L,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ →  Q G L T.
 /4 width=4 by fsb_inv_csx, csx_fsb, fsb_ind_fpbg/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma
index 4dbe33e07..b2093e068 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_fpbg.ma
@@ -38,14 +38,14 @@ lemma fsb_intro_fpbg: ∀h,o,G1,L1,T1. (
 
 (* Eliminators with proper parallel rst-computation for closures ************)
 
-lemma fsb_ind_fpbg_fpbs: ∀h,o. ∀R:relation3 genv lenv term.
+lemma fsb_ind_fpbg_fpbs: ∀h,o. ∀Q:relation3 genv lenv term.
                          (∀G1,L1,T1. ≥[h, o] 𝐒⦃G1, L1, T1⦄ →
-                                     (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
-                                     R G1 L1 T1
+                                     (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → Q G2 L2 T2) →
+                                     Q G1 L1 T1
                          ) →
                          ∀G1,L1,T1. ≥[h, o] 𝐒⦃G1, L1, T1⦄ → 
-                         ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2.
-#h #o #R #IH1 #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1
+                         ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → Q G2 L2 T2.
+#h #o #Q #IH1 #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1
 #G1 #L1 #T1 #H1 #IH #G2 #L2 #T2 #H12
 @IH1 -IH1
 [ -IH /2 width=5 by fsb_fpbs_trans/
@@ -55,12 +55,12 @@ lemma fsb_ind_fpbg_fpbs: ∀h,o. ∀R:relation3 genv lenv term.
 ]
 qed-.
 
-lemma fsb_ind_fpbg: ∀h,o. ∀R:relation3 genv lenv term.
+lemma fsb_ind_fpbg: ∀h,o. ∀Q:relation3 genv lenv term.
                     (∀G1,L1,T1. ≥[h, o] 𝐒⦃G1, L1, T1⦄ →
-                                (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
-                                R G1 L1 T1
+                                (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄ → Q G2 L2 T2) →
+                                Q G1 L1 T1
                     ) →
-                    ∀G1,L1,T1. ≥[h, o] 𝐒⦃G1, L1, T1⦄ → R G1 L1 T1.
-#h #o #R #IH #G1 #L1 #T1 #H @(fsb_ind_fpbg_fpbs … H) -H
+                    ∀G1,L1,T1. ≥[h, o] 𝐒⦃G1, L1, T1⦄ →  Q G1 L1 T1.
+#h #o #Q #IH #G1 #L1 #T1 #H @(fsb_ind_fpbg_fpbs … H) -H
 /3 width=1 by/
 qed-.
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 827a963be..1ee9f365b 100644
--- 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-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lpr.ma
index e442a66b2..120177208 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lpr.ma
@@ -19,15 +19,15 @@ include "basic_2/rt_computation/lprs_tc.ma".
 (* Eliminators with r-transition for full local environments ****************)
 
 (* Basic_2A1: was: lprs_ind_dx *)
-lemma lprs_ind_sn (h) (G) (L2): ∀R:predicate lenv. R L2 →
-                                (∀L1,L. ⦃G, L1⦄ ⊢ ➡[h] L → ⦃G, L⦄ ⊢ ➡*[h] L2 → R L → R L1) →
-                                ∀L1. ⦃G, L1⦄ ⊢ ➡*[h] L2 → R L1.
+lemma lprs_ind_sn (h) (G) (L2): ∀Q:predicate lenv. Q L2 →
+                                (∀L1,L. ⦃G, L1⦄ ⊢ ➡[h] L → ⦃G, L⦄ ⊢ ➡*[h] L2 → Q L → Q L1) →
+                                ∀L1. ⦃G, L1⦄ ⊢ ➡*[h] L2 → Q L1.
 /4 width=8 by lprs_inv_CTC, lprs_CTC, lpr_cprs_trans, cpr_refl, lex_CTC_ind_sn/ qed-.
 
 (* Basic_2A1: was: lprs_ind *)
-lemma lprs_ind_dx (h) (G) (L1): ∀R:predicate lenv. R L1 →
-                                (∀L,L2. ⦃G, L1⦄ ⊢ ➡*[h] L → ⦃G, L⦄ ⊢ ➡[h] L2 → R L → R L2) →
-                                ∀L2. ⦃G, L1⦄ ⊢ ➡*[h] L2 → R L2.
+lemma lprs_ind_dx (h) (G) (L1): ∀Q:predicate lenv. Q L1 →
+                                (∀L,L2. ⦃G, L1⦄ ⊢ ➡*[h] L → ⦃G, L⦄ ⊢ ➡[h] L2 → Q L → Q L2) →
+                                ∀L2. ⦃G, L1⦄ ⊢ ➡*[h] L2 → Q L2.
 /4 width=8 by lprs_inv_CTC, lprs_CTC, lpr_cprs_trans, cpr_refl, lex_CTC_ind_dx/ qed-.
 
 (* Properties with unbound rt-transition for full local environments ********)
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-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpx.ma
index f64f762ee..96def5301 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpx.ma
@@ -36,15 +36,15 @@ lemma lpxs_step_dx (h) (G): ∀L1,L. ⦃G, L1⦄ ⊢ ⬈*[h] L →
 (* Eliminators with unbound rt-transition for full local environments *******)
 
 (* Basic_2A1: was: lpxs_ind_dx *)
-lemma lpxs_ind_sn (h) (G) (L2): ∀R:predicate lenv. R L2 →
-                                (∀L1,L. ⦃G, L1⦄ ⊢ ⬈[h] L → ⦃G, L⦄ ⊢ ⬈*[h] L2 → R L → R L1) →
-                                ∀L1. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → R L1.
+lemma lpxs_ind_sn (h) (G) (L2): ∀Q:predicate lenv. Q L2 →
+                                (∀L1,L. ⦃G, L1⦄ ⊢ ⬈[h] L → ⦃G, L⦄ ⊢ ⬈*[h] L2 → Q L → Q L1) →
+                                ∀L1. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → Q L1.
 /3 width=7 by lpx_cpxs_trans, cpx_refl, lex_CTC_ind_sn/ qed-.
 
 (* Basic_2A1: was: lpxs_ind *)
-lemma lpxs_ind_dx (h) (G) (L1): ∀R:predicate lenv. R L1 →
-                                (∀L,L2. ⦃G, L1⦄ ⊢ ⬈*[h] L → ⦃G, L⦄ ⊢ ⬈[h] L2 → R L → R L2) →
-                                ∀L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → R L2.
+lemma lpxs_ind_dx (h) (G) (L1): ∀Q:predicate lenv. Q L1 →
+                                (∀L,L2. ⦃G, L1⦄ ⊢ ⬈*[h] L → ⦃G, L⦄ ⊢ ⬈[h] L2 → Q L → Q L2) →
+                                ∀L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → Q L2.
 /3 width=7 by lpx_cpxs_trans, cpx_refl, lex_CTC_ind_dx/ qed-.
 
 (* Properties with context-sensitive extended rt-transition for terms *******)
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-.
 
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-.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs.ma
index 22d3b8ebf..59848b068 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs.ma
@@ -28,17 +28,17 @@ interpretation "context-sensitive parallel r-equivalence (term)"
 
 (* Basic_2A1: was: cpcs_ind_dx *)
 lemma cpcs_ind_sn (h) (G) (L) (T2):
-                  ∀R:predicate term. R T2 →
-                  (∀T1,T. ⦃G, L⦄ ⊢ T1 ⬌[h] T → ⦃G, L⦄ ⊢ T ⬌*[h] T2 → R T → R T1) →
-                  ∀T1. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 → R T1.
+                  ∀Q:predicate term. Q T2 →
+                  (∀T1,T. ⦃G, L⦄ ⊢ T1 ⬌[h] T → ⦃G, L⦄ ⊢ T ⬌*[h] T2 → Q T → Q T1) →
+                  ∀T1. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 → Q T1.
 normalize /3 width=6 by TC_star_ind_dx/
 qed-.
 
 (* Basic_2A1: was: cpcs_ind *)
 lemma cpcs_ind_dx (h) (G) (L) (T1):
-                  ∀R:predicate term. R T1 →
-                  (∀T,T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T → ⦃G, L⦄ ⊢ T ⬌[h] T2 → R T → R T2) →
-                  ∀T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 → R T2.
+                  ∀Q:predicate term. Q T1 →
+                  (∀T,T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T → ⦃G, L⦄ ⊢ T ⬌[h] T2 → Q T → Q T2) →
+                  ∀T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 → Q T2.
 normalize /3 width=6 by TC_star_ind/
 qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma
index 8d917e55f..3158b8b03 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma
@@ -289,36 +289,36 @@ qed-.
 
 (* Basic eliminators ********************************************************)
 
-lemma cpm_ind (h): ∀R:relation5 nat genv lenv term term.
-                   (∀I,G,L. R 0 G L (⓪{I}) (⓪{I})) →
-                   (∀G,L,s. R 1 G L (⋆s) (⋆(next h s))) →
-                   (∀n,G,K,V1,V2,W2. ⦃G, K⦄ ⊢ V1 ➡[n, h] V2 → R n G K V1 V2 →
-                     ⬆*[1] V2 ≘ W2 → R n G (K.ⓓV1) (#0) W2
-                   ) → (∀n,G,K,V1,V2,W2. ⦃G, K⦄ ⊢ V1 ➡[n, h] V2 → R n G K V1 V2 →
-                     ⬆*[1] V2 ≘ W2 → R (↑n) G (K.ⓛV1) (#0) W2
-                   ) → (∀n,I,G,K,T,U,i. ⦃G, K⦄ ⊢ #i ➡[n, h] T → R n G K (#i) T →
-                     ⬆*[1] T ≘ U → R n G (K.ⓘ{I}) (#↑i) (U)
+lemma cpm_ind (h): ∀Q:relation5 nat genv lenv term term.
+                   (∀I,G,L. Q 0 G L (⓪{I}) (⓪{I})) →
+                   (∀G,L,s. Q 1 G L (⋆s) (⋆(next h s))) →
+                   (∀n,G,K,V1,V2,W2. ⦃G, K⦄ ⊢ V1 ➡[n, h] V2 → Q n G K V1 V2 →
+                     ⬆*[1] V2 ≘ W2 → Q n G (K.ⓓV1) (#0) W2
+                   ) → (∀n,G,K,V1,V2,W2. ⦃G, K⦄ ⊢ V1 ➡[n, h] V2 → Q n G K V1 V2 →
+                     ⬆*[1] V2 ≘ W2 → Q (↑n) G (K.ⓛV1) (#0) W2
+                   ) → (∀n,I,G,K,T,U,i. ⦃G, K⦄ ⊢ #i ➡[n, h] T → Q n G K (#i) T →
+                     ⬆*[1] T ≘ U → Q n G (K.ⓘ{I}) (#↑i) (U)
                    ) → (∀n,p,I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡[n, h] T2 →
-                     R 0 G L V1 V2 → R n G (L.ⓑ{I}V1) T1 T2 → R n G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2)
+                     Q 0 G L V1 V2 → Q n G (L.ⓑ{I}V1) T1 T2 → Q n G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2)
                    ) → (∀n,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 →
-                     R 0 G L V1 V2 → R n G L T1 T2 → R n G L (ⓐV1.T1) (ⓐV2.T2)
+                     Q 0 G L V1 V2 → Q n G L T1 T2 → Q n G L (ⓐV1.T1) (ⓐV2.T2)
                    ) → (∀n,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[n, h] V2 → ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 →
-                     R n G L V1 V2 → R n G L T1 T2 → R n G L (ⓝV1.T1) (ⓝV2.T2)
-                   ) → (∀n,G,L,V,T1,T,T2. ⦃G, L.ⓓV⦄ ⊢ T1 ➡[n, h] T → R n G (L.ⓓV) T1 T →
-                     ⬆*[1] T2 ≘ T → R n G L (+ⓓV.T1) T2
+                     Q n G L V1 V2 → Q n G L T1 T2 → Q n G L (ⓝV1.T1) (ⓝV2.T2)
+                   ) → (∀n,G,L,V,T1,T,T2. ⦃G, L.ⓓV⦄ ⊢ T1 ➡[n, h] T → Q n G (L.ⓓV) T1 T →
+                     ⬆*[1] T2 ≘ T → Q n G L (+ⓓV.T1) T2
                    ) → (∀n,G,L,V,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 →
-                     R n G L T1 T2 → R n G L (ⓝV.T1) T2
+                     Q n G L T1 T2 → Q n G L (ⓝV.T1) T2
                    ) → (∀n,G,L,V1,V2,T. ⦃G, L⦄ ⊢ V1 ➡[n, h] V2 →
-                     R n G L V1 V2 → R (↑n) G L (ⓝV1.T) V2
+                     Q n G L V1 V2 → Q (↑n) G L (ⓝV1.T) V2
                    ) → (∀n,p,G,L,V1,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L⦄ ⊢ W1 ➡[h] W2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ➡[n, h] T2 →
-                     R 0 G L V1 V2 → R 0 G L W1 W2 → R n G (L.ⓛW1) T1 T2 →
-                     R n G L (ⓐV1.ⓛ{p}W1.T1) (ⓓ{p}ⓝW2.V2.T2)
+                     Q 0 G L V1 V2 → Q 0 G L W1 W2 → Q n G (L.ⓛW1) T1 T2 →
+                     Q n G L (ⓐV1.ⓛ{p}W1.T1) (ⓓ{p}ⓝW2.V2.T2)
                    ) → (∀n,p,G,L,V1,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V → ⦃G, L⦄ ⊢ W1 ➡[h] W2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡[n, h] T2 →
-                     R 0 G L V1 V → R 0 G L W1 W2 → R n G (L.ⓓW1) T1 T2 →
-                     ⬆*[1] V ≘ V2 → R n G L (ⓐV1.ⓓ{p}W1.T1) (ⓓ{p}W2.ⓐV2.T2)
+                     Q 0 G L V1 V → Q 0 G L W1 W2 → Q n G (L.ⓓW1) T1 T2 →
+                     ⬆*[1] V ≘ V2 → Q n G L (ⓐV1.ⓓ{p}W1.T1) (ⓓ{p}W2.ⓐV2.T2)
                    ) →
-                   ∀n,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 → R n G L T1 T2.
-#h #R #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #IH10 #IH11 #IH12 #IH13 #n #G #L #T1 #T2
+                   ∀n,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 → Q n G L T1 T2.
+#h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #IH10 #IH11 #IH12 #IH13 #n #G #L #T1 #T2
 * #c #HC #H generalize in match HC; -HC generalize in match n; -n
 elim H -c -G -L -T1 -T2
 [ #I #G #L #n #H <(isrt_inv_00 … H) -H //
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma
index 5751df0c9..091282ef3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma
@@ -101,29 +101,29 @@ qed-.
 
 (* Basic eliminators ********************************************************)
 
-lemma cpr_ind (h): ∀R:relation4 genv lenv term term.
-                   (∀I,G,L. R G L (⓪{I}) (⓪{I})) →
-                   (∀G,K,V1,V2,W2. ⦃G, K⦄ ⊢ V1 ➡[h] V2 → R G K V1 V2 →
-                     ⬆*[1] V2 ≘ W2 → R G (K.ⓓV1) (#0) W2
-                   ) → (∀I,G,K,T,U,i. ⦃G, K⦄ ⊢ #i ➡[h] T → R G K (#i) T →
-                     ⬆*[1] T ≘ U → R G (K.ⓘ{I}) (#↑i) (U)
+lemma cpr_ind (h): ∀Q:relation4 genv lenv term term.
+                   (∀I,G,L. Q G L (⓪{I}) (⓪{I})) →
+                   (∀G,K,V1,V2,W2. ⦃G, K⦄ ⊢ V1 ➡[h] V2 → Q G K V1 V2 →
+                     ⬆*[1] V2 ≘ W2 → Q G (K.ⓓV1) (#0) W2
+                   ) → (∀I,G,K,T,U,i. ⦃G, K⦄ ⊢ #i ➡[h] T → Q G K (#i) T →
+                     ⬆*[1] T ≘ U → Q G (K.ⓘ{I}) (#↑i) (U)
                    ) → (∀p,I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡[h] T2 →
-                     R G L V1 V2 → R G (L.ⓑ{I}V1) T1 T2 → R G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2)
+                     Q G L V1 V2 → Q G (L.ⓑ{I}V1) T1 T2 → Q G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2)
                    ) → (∀I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L⦄ ⊢ T1 ➡[h] T2 →
-                     R G L V1 V2 → R G L T1 T2 → R G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
-                   ) → (∀G,L,V,T1,T,T2. ⦃G, L.ⓓV⦄ ⊢ T1 ➡[h] T → R G (L.ⓓV) T1 T →
-                     ⬆*[1] T2 ≘ T → R G L (+ⓓV.T1) T2
-                   ) → (∀G,L,V,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 → R G L T1 T2 →
-                     R G L (ⓝV.T1) T2
+                     Q G L V1 V2 → Q G L T1 T2 → Q G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
+                   ) → (∀G,L,V,T1,T,T2. ⦃G, L.ⓓV⦄ ⊢ T1 ➡[h] T → Q G (L.ⓓV) T1 T →
+                     ⬆*[1] T2 ≘ T → Q G L (+ⓓV.T1) T2
+                   ) → (∀G,L,V,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 → Q G L T1 T2 →
+                     Q G L (ⓝV.T1) T2
                    ) → (∀p,G,L,V1,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L⦄ ⊢ W1 ➡[h] W2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ➡[h] T2 →
-                     R G L V1 V2 → R G L W1 W2 → R G (L.ⓛW1) T1 T2 →
-                     R G L (ⓐV1.ⓛ{p}W1.T1) (ⓓ{p}ⓝW2.V2.T2)
+                     Q G L V1 V2 → Q G L W1 W2 → Q G (L.ⓛW1) T1 T2 →
+                     Q G L (ⓐV1.ⓛ{p}W1.T1) (ⓓ{p}ⓝW2.V2.T2)
                    ) → (∀p,G,L,V1,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V → ⦃G, L⦄ ⊢ W1 ➡[h] W2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡[h] T2 →
-                     R G L V1 V → R G L W1 W2 → R G (L.ⓓW1) T1 T2 →
-                     ⬆*[1] V ≘ V2 → R G L (ⓐV1.ⓓ{p}W1.T1) (ⓓ{p}W2.ⓐV2.T2)
+                     Q G L V1 V → Q G L W1 W2 → Q G (L.ⓓW1) T1 T2 →
+                     ⬆*[1] V ≘ V2 → Q G L (ⓐV1.ⓓ{p}W1.T1) (ⓓ{p}W2.ⓐV2.T2)
                    ) →
-                   ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 → R G L T1 T2.
-#h #R #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #G #L #T1 #T2
+                   ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 → Q G L T1 T2.
+#h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #G #L #T1 #T2
 @(insert_eq_0 … 0) #n #H
 @(cpm_ind … H) -G -L -T1 -T2 -n /3 width=4 by/
 [ #G #L #s #H destruct
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma
index f01bb675b..c66c7e94d 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma
@@ -231,31 +231,31 @@ qed-.
 
 (* Basic eliminators ********************************************************)
 
-lemma cpx_ind: ∀h. ∀R:relation4 genv lenv term term.
-               (∀I,G,L. R G L (⓪{I}) (⓪{I})) →
-               (∀G,L,s. R G L (⋆s) (⋆(next h s))) →
-               (∀I,G,K,V1,V2,W2. ⦃G, K⦄ ⊢ V1 ⬈[h] V2 → R G K V1 V2 →
-                 ⬆*[1] V2 ≘ W2 → R G (K.ⓑ{I}V1) (#0) W2
-               ) → (∀I,G,K,T,U,i. ⦃G, K⦄ ⊢ #i ⬈[h] T → R G K (#i) T →
-                 ⬆*[1] T ≘ U → R G (K.ⓘ{I}) (#↑i) (U)
+lemma cpx_ind: ∀h. ∀Q:relation4 genv lenv term term.
+               (∀I,G,L. Q G L (⓪{I}) (⓪{I})) →
+               (∀G,L,s. Q G L (⋆s) (⋆(next h s))) →
+               (∀I,G,K,V1,V2,W2. ⦃G, K⦄ ⊢ V1 ⬈[h] V2 → Q G K V1 V2 →
+                 ⬆*[1] V2 ≘ W2 → Q G (K.ⓑ{I}V1) (#0) W2
+               ) → (∀I,G,K,T,U,i. ⦃G, K⦄ ⊢ #i ⬈[h] T → Q G K (#i) T →
+                 ⬆*[1] T ≘ U → Q G (K.ⓘ{I}) (#↑i) (U)
                ) → (∀p,I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬈[h] T2 →
-                  R G L V1 V2 → R G (L.ⓑ{I}V1) T1 T2 → R G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2)
+                  Q G L V1 V2 → Q G (L.ⓑ{I}V1) T1 T2 → Q G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2)
                ) → (∀I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L⦄ ⊢ T1 ⬈[h] T2 →
-                  R G L V1 V2 → R G L T1 T2 → R G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
-               ) → (∀G,L,V,T1,T,T2. ⦃G, L.ⓓV⦄ ⊢ T1 ⬈[h] T → R G (L.ⓓV) T1 T →
-                  ⬆*[1] T2 ≘ T → R G L (+ⓓV.T1) T2
-               ) → (∀G,L,V,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → R G L T1 T2 →
-                  R G L (ⓝV.T1) T2
-               ) → (∀G,L,V1,V2,T. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → R G L V1 V2 →
-                  R G L (ⓝV1.T) V2
+                  Q G L V1 V2 → Q G L T1 T2 → Q G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
+               ) → (∀G,L,V,T1,T,T2. ⦃G, L.ⓓV⦄ ⊢ T1 ⬈[h] T → Q G (L.ⓓV) T1 T →
+                  ⬆*[1] T2 ≘ T → Q G L (+ⓓV.T1) T2
+               ) → (∀G,L,V,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → Q G L T1 T2 →
+                  Q G L (ⓝV.T1) T2
+               ) → (∀G,L,V1,V2,T. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → Q G L V1 V2 →
+                  Q G L (ⓝV1.T) V2
                ) → (∀p,G,L,V1,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L⦄ ⊢ W1 ⬈[h] W2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈[h] T2 →
-                  R G L V1 V2 → R G L W1 W2 → R G (L.ⓛW1) T1 T2 →
-                  R G L (ⓐV1.ⓛ{p}W1.T1) (ⓓ{p}ⓝW2.V2.T2)
+                  Q G L V1 V2 → Q G L W1 W2 → Q G (L.ⓛW1) T1 T2 →
+                  Q G L (ⓐV1.ⓛ{p}W1.T1) (ⓓ{p}ⓝW2.V2.T2)
                ) → (∀p,G,L,V1,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V → ⦃G, L⦄ ⊢ W1 ⬈[h] W2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈[h] T2 →
-                  R G L V1 V → R G L W1 W2 → R G (L.ⓓW1) T1 T2 →
-                  ⬆*[1] V ≘ V2 → R G L (ⓐV1.ⓓ{p}W1.T1) (ⓓ{p}W2.ⓐV2.T2)
+                  Q G L V1 V → Q G L W1 W2 → Q G (L.ⓓW1) T1 T2 →
+                  ⬆*[1] V ≘ V2 → Q G L (ⓐV1.ⓓ{p}W1.T1) (ⓓ{p}W2.ⓐV2.T2)
                ) →
-               ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → R G L T1 T2.
-#h #R #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #IH10 #IH11 #G #L #T1 #T2
+               ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → Q G L T1 T2.
+#h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #IH10 #IH11 #G #L #T1 #T2
 * #c #H elim H -c -G -L -T1 -T2 /3 width=4 by ex_intro/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqup.ma
index 5f14e8cec..a30e03a45 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqup.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqup.ma
@@ -67,19 +67,19 @@ lemma fqup_flat_dx_bind_dx: ∀b,p,I1,I2,G,L,V1,V2,T. ⦃G, L, ⓕ{I1}V1.ⓑ{p,I
 
 (* Basic eliminators ********************************************************)
 
-lemma fqup_ind: ∀b,G1,L1,T1. ∀R:relation3 ….
-                (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
-                (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊐[b] ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) →
-                ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → R G2 L2 T2.
-#b #G1 #L1 #T1 #R #IH1 #IH2 #G2 #L2 #T2 #H
+lemma fqup_ind: ∀b,G1,L1,T1. ∀Q:relation3 ….
+                (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → Q G2 L2 T2) →
+                (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊐[b] ⦃G2, L2, T2⦄ → Q G L T → Q G2 L2 T2) →
+                ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → Q G2 L2 T2.
+#b #G1 #L1 #T1 #Q #IH1 #IH2 #G2 #L2 #T2 #H
 @(tri_TC_ind … IH1 IH2 G2 L2 T2 H)
 qed-.
 
-lemma fqup_ind_dx: ∀b,G2,L2,T2. ∀R:relation3 ….
-                   (∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → R G1 L1 T1) →
-                   (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ⊐[b] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊐+[b] ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) →
-                   ∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → R G1 L1 T1.
-#b #G2 #L2 #T2 #R #IH1 #IH2 #G1 #L1 #T1 #H
+lemma fqup_ind_dx: ∀b,G2,L2,T2. ∀Q:relation3 ….
+                   (∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → Q G1 L1 T1) →
+                   (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ⊐[b] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊐+[b] ⦃G2, L2, T2⦄ → Q G L T → Q G1 L1 T1) →
+                   ∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → Q G1 L1 T1.
+#b #G2 #L2 #T2 #Q #IH1 #IH2 #G1 #L1 #T1 #H
 @(tri_TC_ind_dx … IH1 IH2 G1 L1 T1 H)
 qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqup_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqup_weight.ma
index 6b1f08b14..69af2d033 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqup_weight.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqup_weight.ma
@@ -27,18 +27,18 @@ qed-.
 
 (* Advanced eliminators *****************************************************)
 
-lemma fqup_wf_ind: ∀b. ∀R:relation3 …. (
-                      ∀G1,L1,T1. (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
-                      R G1 L1 T1
-                   ) → ∀G1,L1,T1. R G1 L1 T1.
-#b #R #HR @(f3_ind … fw) #x #IHx #G1 #L1 #T1 #H destruct
+lemma fqup_wf_ind: ∀b. ∀Q:relation3 …. (
+                      ∀G1,L1,T1. (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → Q G2 L2 T2) →
+                      Q G1 L1 T1
+                   ) → ∀G1,L1,T1. Q G1 L1 T1.
+#b #Q #HQ @(f3_ind … fw) #x #IHx #G1 #L1 #T1 #H destruct
 /4 width=2 by fqup_fwd_fw/
 qed-.
 
-lemma fqup_wf_ind_eq: ∀b. ∀R:relation3 …. (
-                         ∀G1,L1,T1. (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
-                         ∀G2,L2,T2. G1 = G2 → L1 = L2 → T1 = T2 → R G2 L2 T2
-                      ) → ∀G1,L1,T1. R G1 L1 T1.
-#b #R #HR @(f3_ind … fw) #x #IHx #G1 #L1 #T1 #H destruct
+lemma fqup_wf_ind_eq: ∀b. ∀Q:relation3 …. (
+                         ∀G1,L1,T1. (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → Q G2 L2 T2) →
+                         ∀G2,L2,T2. G1 = G2 → L1 = L2 → T1 = T2 → Q G2 L2 T2
+                      ) → ∀G1,L1,T1. Q G1 L1 T1.
+#b #Q #HQ @(f3_ind … fw) #x #IHx #G1 #L1 #T1 #H destruct
 /4 width=7 by fqup_fwd_fw/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqus.ma
index 5cc34a456..32555f1f6 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqus.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/s_computation/fqus.ma
@@ -30,17 +30,17 @@ interpretation "star-iterated structural successor (closure)"
 
 (* Basic eliminators ********************************************************)
 
-lemma fqus_ind: ∀b,G1,L1,T1. ∀R:relation3 …. R G1 L1 T1 →
-                (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊐⸮[b] ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) →
-                ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄ → R G2 L2 T2.
+lemma fqus_ind: ∀b,G1,L1,T1. ∀Q:relation3 …. Q G1 L1 T1 →
+                (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊐⸮[b] ⦃G2, L2, T2⦄ → Q G L T → Q G2 L2 T2) →
+                ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄ → Q G2 L2 T2.
 #b #G1 #L1 #T1 #R #IH1 #IH2 #G2 #L2 #T2 #H
 @(tri_TC_star_ind … IH1 IH2 G2 L2 T2 H) //
 qed-.
 
-lemma fqus_ind_dx: ∀b,G2,L2,T2. ∀R:relation3 …. R G2 L2 T2 →
-                   (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ⊐⸮[b] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊐*[b] ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) →
-                   ∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄ → R G1 L1 T1.
-#b #G2 #L2 #T2 #R #IH1 #IH2 #G1 #L1 #T1 #H
+lemma fqus_ind_dx: ∀b,G2,L2,T2. ∀Q:relation3 …. Q G2 L2 T2 →
+                   (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ⊐⸮[b] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊐*[b] ⦃G2, L2, T2⦄ → Q G L T → Q G1 L1 T1) →
+                   ∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄ → Q G1 L1 T1.
+#b #G2 #L2 #T2 #Q #IH1 #IH2 #G1 #L1 #T1 #H
 @(tri_TC_star_ind_dx … IH1 IH2 G1 L1 T1 H) //
 qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu_weight.ma
index 0ab12e5cc..8f6d321a2 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu_weight.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu_weight.ma
@@ -29,9 +29,9 @@ qed-.
 
 (* Advanced eliminators *****************************************************)
 
-lemma fqu_wf_ind: ∀b. ∀R:relation3 …. (
-                     ∀G1,L1,T1. (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
-		                 R G1 L1 T1
-		              ) → ∀G1,L1,T1. R G1 L1 T1.
-#b #R #HR @(f3_ind … fw) #x #IHx #G1 #L1 #T1 #H destruct /4 width=2 by fqu_fwd_fw/
+lemma fqu_wf_ind: ∀b. ∀Q:relation3 …. (
+                     ∀G1,L1,T1. (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → Q G2 L2 T2) →
+		                 Q G1 L1 T1
+		              ) → ∀G1,L1,T1. Q G1 L1 T1.
+#b #Q #HQ @(f3_ind … fw) #x #IHx #G1 #L1 #T1 #H destruct /4 width=2 by fqu_fwd_fw/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma
index fab29bbe6..217534a14 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma
@@ -100,32 +100,32 @@ elim (pn_split f0) * #g0 #H destruct
 ]
 qed-.
 
-lemma frees_ind_void: ∀R:relation3 ….
+lemma frees_ind_void: ∀Q:relation3 ….
                       (
-                         ∀f,L,s. 𝐈⦃f⦄ → R L (⋆s) f
+                         ∀f,L,s. 𝐈⦃f⦄ →  Q L (⋆s) f
                       ) → (
-                         ∀f,i. 𝐈⦃f⦄ → R (⋆) (#i) (⫯*[i]↑f)
+                         ∀f,i. 𝐈⦃f⦄ →  Q (⋆) (#i) (⫯*[i]↑f)
                       ) → (
                          ∀f,I,L,V.
-                         L ⊢ 𝐅*⦃V⦄ ≘ f → R L V f→ R (L.ⓑ{I}V) (#O) (↑f) 
+                         L ⊢ 𝐅*⦃V⦄ ≘ f →  Q L V f→ Q (L.ⓑ{I}V) (#O) (↑f) 
                       ) → (
-                         ∀f,I,L. 𝐈⦃f⦄ → R (L.ⓤ{I}) (#O) (↑f)
+                         ∀f,I,L. 𝐈⦃f⦄ →  Q (L.ⓤ{I}) (#O) (↑f)
                       ) → (
                          ∀f,I,L,i.
-                         L ⊢ 𝐅*⦃#i⦄ ≘ f → R L (#i) f → R (L.ⓘ{I}) (#(↑i)) (⫯f)
+                         L ⊢ 𝐅*⦃#i⦄ ≘ f →  Q L (#i) f → Q (L.ⓘ{I}) (#(↑i)) (⫯f)
                       ) → (
-                         ∀f,L,l. 𝐈⦃f⦄ → R L (§l) f
+                         ∀f,L,l. 𝐈⦃f⦄ →  Q L (§l) f
                       ) → (
                          ∀f1,f2,f,p,I,L,V,T.
                          L ⊢ 𝐅*⦃V⦄ ≘ f1 → L.ⓧ ⊢𝐅*⦃T⦄≘ f2 → f1 ⋓ ⫱f2 ≘ f →
-                         R L V f1 →R (L.ⓧ) T f2 → R L (ⓑ{p,I}V.T) f
+                         Q L V f1 → Q (L.ⓧ) T f2 → Q L (ⓑ{p,I}V.T) f
                       ) → (
                          ∀f1,f2,f,I,L,V,T.
                          L ⊢ 𝐅*⦃V⦄ ≘ f1 → L ⊢𝐅*⦃T⦄ ≘ f2 → f1 ⋓ f2 ≘ f →
-                         R L V f1 → R L T f2 → R L (ⓕ{I}V.T) f
+                         Q L V f1 → Q L T f2 → Q L (ⓕ{I}V.T) f
                       ) →
-                      ∀L,T,f. L ⊢ 𝐅*⦃T⦄ ≘ f → R L T f.
-#R #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #L #T
+                      ∀L,T,f. L ⊢ 𝐅*⦃T⦄ ≘ f →  Q L T f.
+#Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #L #T
 @(fqup_wf_ind_eq (Ⓕ) … (⋆) L T) -L -T #G0 #L0 #T0 #IH #G #L * *
 [ #s #HG #HL #HT #f #H destruct -IH
   lapply (frees_inv_sort … H) -H /2 width=1 by/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
index cc5b1e623..c9d55b73f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
@@ -272,7 +272,7 @@ lemma lfxs_unit (R): ∀f,I,L1,L2. 𝐈⦃f⦄ → L1 ⪤*[cext2 R, cfull, f] L2
 /4 width=3 by frees_unit, lexs_next, ext2_unit, ex2_intro/ qed.
 
 lemma lfxs_lref (R): ∀I1,I2,L1,L2,i.
-                 L1 ⪤*[R, #i] L2 → L1.ⓘ{I1} ⪤*[R, #↑i] L2.ⓘ{I2}.
+                     L1 ⪤*[R, #i] L2 → L1.ⓘ{I1} ⪤*[R, #↑i] L2.ⓘ{I2}.
 #R #I1 #I2 #L1 #L2 #i * /3 width=3 by lexs_push, frees_lref, ex2_intro/
 qed.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma
index 8e198ac76..76adfa38b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma
@@ -25,9 +25,9 @@ definition f_dedropable_sn: predicate (relation3 lenv term term) ≝
                             ∃∃L2. L1 ⪤*[R, U] L2 & ⬇*[b, f] L2 ≘ K2 & L1 ≡[f] L2.
 
 definition f_dropable_sn: predicate (relation3 lenv term term) ≝
-                        λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≘ K1 → 𝐔⦃f⦄ →
-                        ∀L2,U. L1 ⪤*[R, U] L2 → ∀T. ⬆*[f] T ≘ U →
-                        ∃∃K2. K1 ⪤*[R, T] K2 & ⬇*[b, f] L2 ≘ K2.
+                          λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≘ K1 → 𝐔⦃f⦄ →
+                          ∀L2,U. L1 ⪤*[R, U] L2 → ∀T. ⬆*[f] T ≘ U →
+                          ∃∃K2. K1 ⪤*[R, T] K2 & ⬇*[b, f] L2 ≘ K2.
 
 definition f_dropable_dx: predicate (relation3 lenv term term) ≝
                           λR. ∀L1,L2,U. L1 ⪤*[R, U] L2 →
diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/append_length.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/append_length.ma
index c1133e8c0..e7c79ebee 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/syntax/append_length.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/append_length.ma
@@ -103,9 +103,9 @@ qed-.
 
 (* Basic_1: was: c_tail_ind *)
 (* Basic_2A1: was: lenv_ind_alt *) 
-lemma lenv_ind_tail: ∀R:predicate lenv.
-                     R (⋆) → (∀I,L. R L → R (ⓘ{I}.L)) → ∀L. R L.
-#R #IH1 #IH2 #L @(f_ind … length … L) -L #x #IHx * //
+lemma lenv_ind_tail: ∀Q:predicate lenv.
+                     Q (⋆) → (∀I,L. Q L → Q (ⓘ{I}.L)) → ∀L. Q L.
+#Q #IH1 #IH2 #L @(f_ind … length … L) -L #x #IHx * //
 #L #I -IH1 #H destruct
 elim (lenv_case_tail … L) [2: * #K #J ]
 #H destruct /3 width=1 by/
-- 
2.39.2