X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_conversion%2Fcpc_cpc.ma;h=d3151122a0bf9560eece7f5c586535f4488fc208;hp=b5b9ac86c0a8552331c665f121c037e73bddaed1;hb=f308429a0fde273605a2330efc63268b4ac36c99;hpb=87f57ddc367303c33e19c83cd8989cd561f3185b

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpc_cpc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpc_cpc.ma
index b5b9ac86c..d3151122a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpc_cpc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpc_cpc.ma
@@ -18,6 +18,6 @@ include "basic_2/rt_conversion/cpc.ma".
 
 (* Main properties **********************************************************)
 
-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.
+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-.