cicInspect: node count fixed

[helm.git] / helm / software / matita / contribs / character / classes / props_pt.ma

diff --git a/helm/software/matita/contribs/character/classes/props_pt.ma b/helm/software/matita/contribs/character/classes/props_pt.ma
index cc1c449a3339babbffc6b10a9d8dcd203ce6b0c1..64b424ae3c71b7f8fd173594ef3e449a7bbc2662 100644 (file)
--- a/helm/software/matita/contribs/character/classes/props_pt.ma
+++ b/helm/software/matita/contribs/character/classes/props_pt.ma
@@ -62,7 +62,7 @@ theorem pt_inv_gen: \forall i.
  [ lapply linear p_inv_O to H; decompose
  | lapply linear t_inv_O to H; decompose
  | inversion H1; clear H1; intros;
-   [ destruct; autobatch depth = 3
+   [ destruct; autobatch depth = 3 width = 50 size = 50
    | clear H3; lapply t_pos to H1; lapply p_pos to H2; decompose; destruct;
      lapply linear plus_inv_S_S_S to H4; decompose;
      lapply H to H4; lapply H to H3; clear H H4 H3; decompose; clear H3 H4;