X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fconversion%2Fcpc_cpc.ma;h=92ce08e18e365260348730493834c2729a37acfd;hb=632c54beaf67e68a1eeeec22274466157003b779;hp=14518aaabdd4660eed4cc4bbeca927e61b5a64ad;hpb=d0e3208d69d24a9dc9e066e381f1601bc8e109be;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc_cpc.ma b/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc_cpc.ma
index 14518aaab..92ce08e18 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc_cpc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc_cpc.ma
@@ -14,10 +14,10 @@
 
 include "basic_2/conversion/cpc.ma".
 
-(* CONTEXT-SENSITIVE PARALLEL CONVERSION ON TERMS ***************************)
+(* CONTEXT-SENSITIVE PARALLEL R-CONVERSION FOR TERMS ************************)
 
 (* Main properties **********************************************************)
 
-theorem cpc_conf: ∀G,L,T0,T1,T2. ⦃G, L⦄ ⊢ T0 ⬌ T1 → ⦃G, L⦄ ⊢ T0 ⬌ T2 →
-                  ∃∃T. ⦃G, L⦄ ⊢ T1 ⬌ T & ⦃G, L⦄ ⊢ T2 ⬌ T.
+theorem cpc_conf: ∀h,G,L,T0,T1,T2. ⦃G, L⦄ ⊢ T0 ⬌[h] T1 → ⦃G, L⦄ ⊢ T0 ⬌[h] T2 →
+                  ∃∃T. ⦃G, L⦄ ⊢ T1 ⬌[h] T & ⦃G, L⦄ ⊢ T2 ⬌[h] T.
 /3 width=3 by cpc_sym, ex2_intro/ qed-.