X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fconversion%2Fcpc_cpc.ma;h=714d3e712a8fee6319471ad9316d6e7a395d93e7;hb=6f1f9e20aa2775d41bba64289fc903e6612baaf3;hp=092d2a9a753d9dffad0cc61eece486add6552ecd;hpb=29973426e0227ee48368d1c24dc0c17bf2baef77;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 092d2a9a7..714d3e712 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc_cpc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc_cpc.ma
@@ -18,6 +18,6 @@ include "basic_2/conversion/cpc.ma".
 
 (* Main properties **********************************************************)
 
-theorem cpc_conf: ∀L,T0,T1,T2. ⦃G, L⦄ ⊢ T0 ⬌ T1 → ⦃G, L⦄ ⊢ T0 ⬌ T2 →
+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.
-/3 width=3/ qed.
+/3 width=3/ qed-.