old subst tactics removed. New destruct tactic used instead

diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fun.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fun.ma
index c88b2f92685d33fd15c5ad9cd63058e538b72562..86e8031b41d947562fdac57d32022d38680d896d 100644 (file)
--- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fun.ma
+++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fun.ma
@@ -39,7 +39,7 @@ theorem lift_mono: \forall l,i,t,t1. Lift l i t t1 \to
  | lapply linear lift_inv_lref_1_le_nplus to H3, H1, H2
  | lapply linear lift_inv_bind_1 to H5. decompose
  | lapply linear lift_inv_flat_1 to H5. decompose
- ]; subst; autobatch.
+ ]; destruct; autobatch.
 qed.
 
 theorem lift_inj: \forall l,i,t1,t. Lift l i t1 t \to
@@ -53,5 +53,5 @@ theorem lift_inj: \forall l,i,t1,t. Lift l i t1 t \to
    lapply lift_inv_lref_2_le_nplus to H3, H0, H2
  | lapply linear lift_inv_bind_2 to H5. decompose
  | lapply linear lift_inv_flat_2 to H5. decompose
- ]; subst; autobatch.
+ ]; destruct; autobatch.
 qed.

diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma
index 87b7bdc8c1a1241d7e4547f6c0f040452f6980c1..95630e43e4cd8ae73dc2223d04e1c36a4cc86539 100644 (file)
--- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma
+++ b/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. autobatch.
+ intros. inversion H; clear H; intros; destruct. autobatch.
 qed.
 
 theorem lift_inv_lref_1: \forall l, i, j1, x.
@@ -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 size = 7.
+ intros. inversion H; clear H; intros; destruct; 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 size = 7.
+ intros. inversion H; clear H; intros; destruct; autobatch depth = 5 size = 7.
 qed.
 
 theorem lift_inv_flat_1: \forall l, i, r, u1, t1, x.
@@ -48,13 +48,13 @@ 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 size = 7.
+ intros. inversion H; clear H; intros; destruct. autobatch depth = 5 size = 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. autobatch.
+ intros. inversion H; clear H; intros; destruct. autobatch.
 qed.
 
 theorem lift_inv_lref_2: \forall l, i, x, j2.
@@ -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 size = 10.
+ intros. inversion H; clear H; intros; destruct; 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 size = 7.
+ intros. inversion H; clear H; intros; destruct. 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 size = 7.
+ intros. inversion H; clear H; intros; destruct. autobatch depth = 5 size = 7.
 qed.
 
 (* Corollaries of inversion properties ***************************************)
@@ -90,7 +90,7 @@ theorem lift_inv_lref_1_gt: \forall l, i, j1, x.
                             Lift l i (lref j1) x \to
                             i > j1 \to x = lref j1.
  intros.
- lapply linear lift_inv_lref_1 to H. decompose; subst;
+ lapply linear lift_inv_lref_1 to H. decompose; destruct;
  [ autobatch
  | lapply linear nle_false to H2, H1. decompose
  ].
@@ -100,7 +100,7 @@ theorem lift_inv_lref_1_le: \forall l, i, j1, x.
                             Lift l i (lref j1) x \to i <= j1 \to 
                             \exists j2. (l + j1 == j2) \land x = lref j2.
  intros.
- lapply linear lift_inv_lref_1 to H. decompose; subst;
+ lapply linear lift_inv_lref_1 to H. decompose; destruct;
  [ lapply linear nle_false to H1, H2. decompose
  | autobatch
  ].
@@ -111,9 +111,9 @@ theorem lift_inv_lref_1_le_nplus: \forall l, i, j1, x.
                                  i <= j1 \to \forall j2. (l + j1 == j2) \to
                                  x = lref j2.
  intros.
- lapply linear lift_inv_lref_1 to H. decompose; subst;
+ lapply linear lift_inv_lref_1 to H. decompose; destruct;
  [ lapply linear nle_false to H1, H3. decompose
- | lapply linear nplus_mono to H2, H4. subst. autobatch
+ | lapply linear nplus_mono to H2, H4. destruct. autobatch
  ].
 qed.
 
@@ -121,7 +121,7 @@ theorem lift_inv_lref_2_gt: \forall l, i, x, j2.
                             Lift l i x (lref j2) \to
                             i > j2 \to x = lref j2.
  intros.
- lapply linear lift_inv_lref_2 to H. decompose; subst;
+ lapply linear lift_inv_lref_2 to H. decompose; destruct;
  [ autobatch
  | lapply linear nle_false to H2, H1. decompose
  ].
@@ -131,7 +131,7 @@ theorem lift_inv_lref_2_le: \forall l, i, x, j2.
                             Lift l i x (lref j2) \to i <= j2 \to 
                             \exists j1. (l + j1 == j2) \land x = lref j1.
  intros.
- lapply linear lift_inv_lref_2 to H. decompose; subst;
+ lapply linear lift_inv_lref_2 to H. decompose; destruct;
  [ lapply linear nle_false to H1, H2. decompose
  | autobatch
  ].
@@ -142,8 +142,8 @@ theorem lift_inv_lref_2_le_nplus: \forall l, i, x, j2.
                                   i <= j2 \to \forall j1. (l + j1 == j2) \to
                                   x = lref j1.
  intros.
- lapply linear lift_inv_lref_2 to H. decompose; subst;
+ lapply linear lift_inv_lref_2 to H. decompose; destruct;
  [ lapply linear nle_false to H1, H3. decompose
- | lapply linear nplus_inj_2 to H2, H4. subst. autobatch
+ | lapply linear nplus_inj_2 to H2, H4. destruct. autobatch
  ].
 qed.

diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/props.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/props.ma
index 47345e288e73c802fa2f3f223bce3429e8e5fa68..9df9cbd63712b48b5e4a5639bf46eee7ad2676f2 100644 (file)
--- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/props.ma
+++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/props.ma
@@ -23,27 +23,27 @@ theorem lift_comp: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to
                    \forall i,y. Lift l1 i u1 y \to
                    i1 >= i2 \to (l2 + i1 == i) \to x = y.
  intros 5. elim H; clear H i1 t1 t2;
- [ lapply lift_mono to H1, H2. clear H2. subst.
-   lapply linear lift_inv_sort_1 to H1. subst.
-   lapply linear lift_inv_sort_1 to H3. subst. autobatch
- | lapply lift_mono to H2, H3. clear H3. subst.
+ [ lapply lift_mono to H1, H2. clear H2. destruct.
+   lapply linear lift_inv_sort_1 to H1. destruct.
+   lapply linear lift_inv_sort_1 to H3. destruct. autobatch
+ | lapply lift_mono to H2, H3. clear H3. destruct.
    lapply linear lift_inv_lref_1 to H2.
-   decompose; subst; clear H2 H5;
-   lapply linear lift_inv_lref_1_gt to H4; subst; autobatch width = 4
+   decompose; destruct; clear H2 H5;
+   lapply linear lift_inv_lref_1_gt to H4; destruct; autobatch width = 4
  | lapply lift_inv_lref_1_le to H3; [ 2: autobatch ]. clear H3.
    lapply lift_inv_lref_1_le to H4; [ 2: autobatch ]. clear H4.
-   decompose. subst. clear H6 i2.
+   decompose. destruct. clear H6 i2.
    lapply lift_inv_lref_1_le to H5; [ 2: autobatch depth = 4 width = 4 ]. 
-   decompose. subst. clear H5 H1 H7 i. autobatch depth = 4 size = 7
+   decompose. destruct. clear H5 H1 H7 i. autobatch depth = 4 size = 7
  | clear H1 H3.
    lapply linear lift_inv_bind_1 to H5.
-   lapply linear lift_inv_bind_1 to H6. decompose. subst.
-   lapply linear lift_inv_bind_1 to H7. decompose. subst.
+   lapply linear lift_inv_bind_1 to H6. decompose. destruct.
+   lapply linear lift_inv_bind_1 to H7. decompose. destruct.
    autobatch depth = 4 width = 6 size = 15
  | clear H1 H3.
    lapply linear lift_inv_flat_1 to H5.
-   lapply linear lift_inv_flat_1 to H6. decompose. subst.
-   lapply linear lift_inv_flat_1 to H7. decompose. subst.
+   lapply linear lift_inv_flat_1 to H6. decompose. destruct.
+   lapply linear lift_inv_flat_1 to H7. decompose. destruct.
    autobatch depth = 4 width = 6 size = 9
  ].
 qed.
@@ -55,7 +55,7 @@ theorem lift_comp_rew_dx: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to
                           Lift l1 i u1 u2.
  intros.
  lapply (lift_total l1 u1 i). decompose.
- lapply lift_comp to H, H1, H2, H5, H3, H4. subst. autobatch.
+ lapply lift_comp to H, H1, H2, H5, H3, H4. destruct. autobatch.
 qed.
 
 theorem lift_comp_rew_sx: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to
@@ -65,7 +65,7 @@ theorem lift_comp_rew_sx: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to
                           Lift l1 i1 u1 u2.
  intros.
  lapply (lift_total l1 u1 i1). decompose.
- lapply lift_comp to H1, H, H5, H2, H3, H4. subst. autobatch.
+ lapply lift_comp to H1, H, H5, H2, H3, H4. destruct. autobatch.
 qed.
 (*
 theorem lift_trans_le: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to