X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FLAMBDA-TYPES%2FUnified-Sub%2FLift%2Fprops.ma;h=9df9cbd63712b48b5e4a5639bf46eee7ad2676f2;hb=cd85befa31c33698c57d5d5d0d7a2384bb2644f9;hp=47345e288e73c802fa2f3f223bce3429e8e5fa68;hpb=b2abc81f0b76224f6f4f526feaf1fefd6178ae7d;p=helm.git

diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/props.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/props.ma
index 47345e288..9df9cbd63 100644
--- 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