- the trace is explicit in all auto tactics with depth > 1

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / conversion / cpc.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc.ma b/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc.ma
index 116e159502e110892c099d71bec242d5c6a84396..1268d8887ab0a535da4271d0111bb7ff4d6c7894 100644 (file)
--- 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-.