X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FUnified-Sub%2FLift%2Finv.ma;h=87b7bdc8c1a1241d7e4547f6c0f040452f6980c1;hb=49e72b6a1c126e7e34323b64decad10d46d93f97;hp=35540f87ae8cd59d698c3f93d7737e8a8afffd8f;hpb=a861d697fb8c13f8b12507a576aba03d0b33024c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma
index 35540f87a..87b7bdc8c 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma
+++ b/helm/software/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; autobatch depth = 5.
+ intros. inversion H; clear H; intros; subst; autobatch depth = 5 size = 7.
 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. autobatch depth = 5.
+ intros. inversion H; clear H; intros; subst; autobatch depth = 5 size = 7.
 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. autobatch depth = 5.
+ intros. inversion H; clear H; intros; subst. autobatch depth = 5 size = 7.
 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; autobatch depth = 5.
+ intros. inversion H; clear H; intros; subst; autobatch depth = 5 size = 10.
 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. autobatch depth = 5.
+ intros. inversion H; clear H; intros; subst. autobatch depth = 5 size = 7.
 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. autobatch depth = 5.
+ intros. inversion H; clear H; intros; subst. autobatch depth = 5 size = 7.
 qed.
 
 (* Corollaries of inversion properties ***************************************)