auto --> autobatch

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

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 3a48e5987353aeff75e5ecf626b95bf92c723ec7..b39e419ad6dc0d5fa2fd8553e54f556faeb9d58d 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma
@@ -21,7 +21,7 @@ include "Lift/defs.ma".
 theorem lift_inv_sort_1: \forall l, i, h, x.
                          Lift l i (sort h) x \to
                          x = sort h.
- intros. inversion H; clear H; intros; subst. auto.
+ intros. inversion H; clear H; intros; subst. autobatch.
 qed.
 
 theorem lift_inv_lref_1: \forall l, i, j1, x.
@@ -54,7 +54,7 @@ qed.
 theorem lift_inv_sort_2: \forall l, i, x, h.
                          Lift l i x (sort h) \to
                          x = sort h.
- intros. inversion H; clear H; intros; subst. auto.
+ intros. inversion H; clear H; intros; subst. autobatch.
 qed.
 
 theorem lift_inv_lref_2: \forall l, i, x, j2.