X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fconversion%2Fcpc.ma;h=1268d8887ab0a535da4271d0111bb7ff4d6c7894;hb=37e1b4f314ffae815beca71300688040f8da6939;hp=116e159502e110892c099d71bec242d5c6a84396;hpb=c60524dec7ace912c416a90d6b926bee8553250b;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc.ma b/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc.ma
index 116e15950..1268d8887 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc.ma
@@ -27,14 +27,14 @@ interpretation
 (* Basic properties *********************************************************)
 
 lemma cpc_refl: ∀G,L. reflexive … (cpc G L).
-/2 width=1/ qed.
+/2 width=1 by or_intror/ qed.
 
 lemma cpc_sym: ∀G,L. symmetric … (cpc L G).
-#G #L #T1 #T2 * /2 width=1/
-qed.
+#G #L #T1 #T2 * /2 width=1 by or_introl, or_intror/
+qed-.
 
 (* Basic forward lemmas *****************************************************)
 
 lemma cpc_fwd_cpr: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌ T2 → ∃∃T. ⦃G, L⦄ ⊢ T1 ➡ T & ⦃G, L⦄ ⊢ T2 ➡ T.
-#G #L #T1 #T2 * /2 width=3/
+#G #L #T1 #T2 * /2 width=3 by ex2_intro/
 qed-.