- Procedural: we now reconstruct "let H := v in t" with "intros (1) H" when the goal...

[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 82526c26aca67067caca0bbc4ba9a90ccc0c7534..58fbaf300843d3011d946be0065ad9ab78a6212e 100644 (file)
--- 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
  ].