X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fcharacter%2Fclasses%2Fprops_pt.ma;h=58fbaf300843d3011d946be0065ad9ab78a6212e;hb=a88be1ca42c0969dbab9a5c76240f5931df876d9;hp=82526c26aca67067caca0bbc4ba9a90ccc0c7534;hpb=04f75822f22c6c6522f6d81b412a212885a6ff72;p=helm.git

diff --git a/helm/software/matita/contribs/character/classes/props_pt.ma b/helm/software/matita/contribs/character/classes/props_pt.ma
index 82526c26a..58fbaf300 100644
--- a/helm/software/matita/contribs/character/classes/props_pt.ma
+++ b/helm/software/matita/contribs/character/classes/props_pt.ma
@@ -15,11 +15,10 @@
 include "classes/defs.ma".
 
 theorem p_inv_O: P 0 → False.
- intros; inversion H; clear H; intros;
- [ destruct
- | lapply linear plus_inv_O3 to H3; decompose; destruct; 
-   autobatch depth = 2
- ].
+ intros; inversion H;intros;
+ [apply (not_eq_O_S ? H1)
+ |autobatch.
+ ]
 qed.
 
 theorem t_inv_O: T 0 → False.
@@ -30,7 +29,7 @@ theorem t_inv_O: T 0 → False.
 qed.
 
 theorem p_pos: ∀i. P i → ∃k. i = S k.
- intros 1; elim i names 0; clear i; intros;
+ intros 1; elim i 0; clear i; intros;
  [ lapply linear p_inv_O to H; decompose
  | autobatch depth = 2
  ].