X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fconversion%2Fcpc_cpc.ma;h=14518aaabdd4660eed4cc4bbeca927e61b5a64ad;hb=37e1b4f314ffae815beca71300688040f8da6939;hp=714d3e712a8fee6319471ad9316d6e7a395d93e7;hpb=c60524dec7ace912c416a90d6b926bee8553250b;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 714d3e712..14518aaab 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc_cpc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc_cpc.ma
@@ -20,4 +20,4 @@ include "basic_2/conversion/cpc.ma".
 
 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 by cpc_sym, ex2_intro/ qed-.