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

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reduction / cpr.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma
index 61d8fd9317d55a6493b29ccc37b8f8e78d2ca963..6dafc6d8c515968ba9f6941e723eaaefc4717e55 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma
@@ -264,7 +264,7 @@ lemma cpr_inv_appl1_simple: ∀G,L,V1,T1,U. ⦃G, L⦄ ⊢ ⓐV1. T1 ➡ U → 
                                      U = ⓐV2. T2.
 #G #L #V1 #T1 #U #H #HT1
 elim (cpr_inv_appl1 … H) -H *
-[ /2 width=5/
+[ /2 width=5 by ex3_2_intro/
 | #a #V2 #W1 #W2 #U1 #U2 #_ #_ #_ #H #_ destruct
   elim (simple_inv_bind … HT1)
 | #a #V #V2 #W1 #W2 #U1 #U2 #_ #_ #_ #_ #H #_ destruct