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

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / substitution / gget_gget.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/gget_gget.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/gget_gget.ma
index c08ab3960bc193989bb754b704e4acf774600cac..7bd39f09b33a5fea8f10bd4d9b6a912fe17ab7a1 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/gget_gget.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/gget_gget.ma
@@ -25,7 +25,7 @@ theorem gget_mono: ∀G,G1,m. ⬇[m] G ≡ G1 → ∀G2. ⬇[m] G ≡ G2 → G1
 | #G #Hm #G2 #H
   >(gget_inv_eq … H Hm) -H -Hm //
 | #I #G #G1 #V #Hm #_ #IHG1 #G2 #H
-  lapply (gget_inv_lt … H Hm) -H -Hm /2 width=1/
+  lapply (gget_inv_lt … H Hm) -H -Hm /2 width=1 by/
 ]
 qed-.
 
@@ -33,8 +33,8 @@ lemma gget_dec: ∀G1,G2,m. Decidable (⬇[m] G1 ≡ G2).
 #G1 #G2 #m
 elim (gget_total m G1) #G #HG1
 elim (eq_genv_dec G G2) #HG2
-[ destruct /2 width=1/
+[ destruct /2 width=1 by or_introl/
 | @or_intror #HG12
-  lapply (gget_mono … HG1 … HG12) -HG1 -HG12 /2 width=1/
+  lapply (gget_mono … HG1 … HG12) -HG1 -HG12 /2 width=1 by/
 ]
 qed-.