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

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma
index 576633954bd138547b93255e7853daeb456eb579..ba5ba7e7e8aeacef8f67be60d84b2f8cb2355143 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma
@@ -43,7 +43,7 @@ qed-.
 
 lemma cir_inv_appl: ∀G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐈⦃ⓐV.T⦄ →
                     ∧∧ ⦃G, L⦄ ⊢ ➡ 𝐈⦃V⦄ & ⦃G, L⦄ ⊢ ➡ 𝐈⦃T⦄ & 𝐒⦃T⦄.
-#G #L #V #T #HVT @and3_intro /3 width=1/
+#G #L #V #T #HVT @and3_intro /3 width=1 by crr_appl_sn, crr_appl_dx/
 generalize in match HVT; -HVT elim T -T //
 * // #a * #U #T #_ #_ #H elim H -H /2 width=1 by crr_beta, crr_theta/
 qed-.