X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_equivalence%2Fcpcs.ma;h=59848b0680c2325e3ce4437a644c6f53e857146e;hp=22d3b8ebf7abbecc41cdbb4c9b03a0b636dd9dfb;hb=5c186c72f508da0849058afeecc6877cd9ed6303;hpb=282511a928532676813d99d08594cd5f98fcb80e

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-.