some old auto yurned into autobatch

[helm.git] / matita / contribs / LAMBDA-TYPES / Unified-Sub / Lift / inv.ma

diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma
index b39e419ad6dc0d5fa2fd8553e54f556faeb9d58d..35540f87ae8cd59d698c3f93d7737e8a8afffd8f 100644 (file)
--- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma
+++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma
@@ -30,7 +30,7 @@ theorem lift_inv_lref_1: \forall l, i, j1, x.
                          (i <= j1 \land 
                           \exists j2. (l + j1 == j2) \land x = lref j2
                          ).
- intros. inversion H; clear H; intros; subst; auto depth = 5.
+ intros. inversion H; clear H; intros; subst; autobatch depth = 5.
 qed.
 
 theorem lift_inv_bind_1: \forall l, i, r, u1, t1, x.
@@ -39,7 +39,7 @@ theorem lift_inv_bind_1: \forall l, i, r, u1, t1, x.
                          Lift l i u1 u2 \land
                          Lift l (succ i) t1 t2 \land
                          x = intb r u2 t2.
- intros. inversion H; clear H; intros; subst. auto depth = 5.
+ intros. inversion H; clear H; intros; subst. autobatch depth = 5.
 qed.
 
 theorem lift_inv_flat_1: \forall l, i, r, u1, t1, x.
@@ -48,7 +48,7 @@ theorem lift_inv_flat_1: \forall l, i, r, u1, t1, x.
                          Lift l i u1 u2 \land
                          Lift l i t1 t2 \land
                          x = intf r u2 t2.
- intros. inversion H; clear H; intros; subst. auto depth = 5.
+ intros. inversion H; clear H; intros; subst. autobatch depth = 5.
 qed.
 
 theorem lift_inv_sort_2: \forall l, i, x, h.
@@ -63,7 +63,7 @@ theorem lift_inv_lref_2: \forall l, i, x, j2.
                          (i <= j2 \land 
                           \exists j1. (l + j1 == j2) \land x = lref j1
                          ).
- intros. inversion H; clear H; intros; subst; auto depth = 5.
+ intros. inversion H; clear H; intros; subst; autobatch depth = 5.
 qed.
 
 theorem lift_inv_bind_2: \forall l, i, r, x, u2, t2.
@@ -72,7 +72,7 @@ theorem lift_inv_bind_2: \forall l, i, r, x, u2, t2.
                          Lift l i u1 u2 \land
                          Lift l (succ i) t1 t2 \land
                          x = intb r u1 t1.
- intros. inversion H; clear H; intros; subst. auto depth = 5.
+ intros. inversion H; clear H; intros; subst. autobatch depth = 5.
 qed.
 
 theorem lift_inv_flat_2: \forall l, i, r, x, u2, t2.
@@ -81,7 +81,7 @@ theorem lift_inv_flat_2: \forall l, i, r, x, u2, t2.
                          Lift l i u1 u2 \land
                          Lift l i t1 t2 \land
                          x = intf r u1 t1.
- intros. inversion H; clear H; intros; subst. auto depth = 5.
+ intros. inversion H; clear H; intros; subst. autobatch depth = 5.
 qed.
 
 (* Corollaries of inversion properties ***************************************)
@@ -91,7 +91,7 @@ theorem lift_inv_lref_1_gt: \forall l, i, j1, x.
                             i > j1 \to x = lref j1.
  intros.
  lapply linear lift_inv_lref_1 to H. decompose; subst;
- [ auto
+ [ autobatch
  | lapply linear nle_false to H2, H1. decompose
  ].
 qed.
@@ -102,7 +102,7 @@ theorem lift_inv_lref_1_le: \forall l, i, j1, x.
  intros.
  lapply linear lift_inv_lref_1 to H. decompose; subst;
  [ lapply linear nle_false to H1, H2. decompose
- | auto
+ | autobatch
  ].
 qed.
 
@@ -113,7 +113,7 @@ theorem lift_inv_lref_1_le_nplus: \forall l, i, j1, x.
  intros.
  lapply linear lift_inv_lref_1 to H. decompose; subst;
  [ lapply linear nle_false to H1, H3. decompose
- | lapply linear nplus_mono to H2, H4. subst. auto
+ | lapply linear nplus_mono to H2, H4. subst. autobatch
  ].
 qed.
 
@@ -122,7 +122,7 @@ theorem lift_inv_lref_2_gt: \forall l, i, x, j2.
                             i > j2 \to x = lref j2.
  intros.
  lapply linear lift_inv_lref_2 to H. decompose; subst;
- [ auto
+ [ autobatch
  | lapply linear nle_false to H2, H1. decompose
  ].
  qed.
@@ -133,7 +133,7 @@ theorem lift_inv_lref_2_le: \forall l, i, x, j2.
  intros.
  lapply linear lift_inv_lref_2 to H. decompose; subst;
  [ lapply linear nle_false to H1, H2. decompose
- | auto
+ | autobatch
  ].
 qed.
 
@@ -144,6 +144,6 @@ theorem lift_inv_lref_2_le_nplus: \forall l, i, x, j2.
  intros.
  lapply linear lift_inv_lref_2 to H. decompose; subst;
  [ lapply linear nle_false to H1, H3. decompose
- | lapply linear nplus_inj_2 to H2, H4. subst. auto
+ | lapply linear nplus_inj_2 to H2, H4. subst. autobatch
  ].
 qed.