Via un'altra linea...

diff --git a/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion3.ma b/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion3.ma
index be3033199032948abeb85873badc93cc76dca3a2..14f1525a7cbe64d1327660087d81488d1f8d88df 100644 (file)
--- a/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion3.ma
+++ b/helm/software/matita/contribs/POPLmark/Fsub/part1a_inversion3.ma
@@ -50,7 +50,7 @@ lemma JSubtype_inv:
  intros;
  generalize in match (refl_eq ? T);
  generalize in match (refl_eq ? G);
- elim H5 in ⊢ (? ? ? % → ? ? ? % → %); destruct; autobatch depth=3 width=4 size=7;
+ elim H5 in ⊢ (? ? ? % → ? ? ? % → %); destruct; autobatch width=4 size=7;
 qed.
 
 theorem narrowing:∀X,G,G1,U,P,M,N.