X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fty0_subst0.v;h=ffd80110bf4c0dc6591540932d98f980b92a8476;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=3e4703200b001c75c1af7d9aa5653e131a7af029;hpb=1b21075e987872a2e3103203b4e67c939e4a9f6a;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/ty0_subst0.v b/helm/coq-contribs/LAMBDA-TYPES/ty0_subst0.v
index 3e4703200..ffd80110b 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/ty0_subst0.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/ty0_subst0.v
@@ -1,8 +1,10 @@
 Require drop_props.
 Require csubst0_defs.
+Require fsubst0_defs.
 Require pc3_props.
 Require pc3_subst0.
 Require ty0_defs.
+Require ty0_gen.
 Require ty0_lift.
 Require ty0_props.
 
@@ -128,36 +130,36 @@ Require ty0_props.
       Intros until 1; XElim H.
 (* case 1: ty0_conv *)
       Intros until 6; XElim H4; Intros.
-(* case 1.1: fsubst0_t *)
+(* case 1.1: fsubst0_snd *)
       IHT; EApply ty0_conv; XEAuto.
-(* case 1.2: fsubst0_c *)
+(* case 1.2: fsubst0_fst *)
       IHC; EApply ty0_conv; Try EApply pc3_fsubst0; XEAuto.
-(* case 1.3: fsubst0_b *)
+(* case 1.3: fsubst0_both *)
       IHCT; IHCT; EApply ty0_conv; Try EApply pc3_fsubst0; XEAuto.
 (* case 2: ty0_sort *)
       Intros until 2; XElim H0; Intros.
-(* case 2.1: fsubst0_t *)
+(* case 2.1: fsubst0_snd *)
       Subst0GenBase.
-(* case 2.2: fsubst0_c *)
+(* case 2.2: fsubst0_fst *)
       XAuto.
-(* case 2.3: fsubst0_b *)
+(* case 2.3: fsubst0_both *)
       Subst0GenBase.
 (* case 3: ty0_abbr *)
       Intros until 5; XElim H3; Intros; Clear c1 c2 t t1 t2.
-(* case 3.1: fsubst0_t *)
+(* case 3.1: fsubst0_snd *)
       Subst0GenBase; Rewrite H6; Rewrite <- H3 in H5; Clear H3 H6 i t3.
       DropDis; Inversion H5; Rewrite <- H6 in H0; Rewrite H7 in H1; XEAuto.
-(* case 3.2: fsubst0_c *)
+(* case 3.2: fsubst0_fst *)
       Apply (lt_le_e n i); Intros; CSubst0Drop.
 (* case 3.2.1: n < i, none *)
       EApply ty0_abbr; XEAuto.
-(* case 3.2.2: n < i, csubst0_fst *)
+(* case 3.2.2: n < i, csubst0_snd *)
       Inversion H0; CSubst0Drop.
       Rewrite <- H10 in H7; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H8;
       Clear H0 H10 H11 H12 x0 x1 x2.
       DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase | XAuto ].
       IHT; EApply ty0_abbr; XEAuto.
-(* case 3.2.3: n < i, csubst0_snd *)
+(* case 3.2.3: n < i, csubst0_fst *)
       Inversion H0; CSubst0Drop.
       Rewrite <- H10 in H8; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H7;
       Clear H0 H10 H11 H12 x0 x1 x3.
@@ -171,26 +173,26 @@ Require ty0_props.
       IHCT; EApply ty0_abbr; XEAuto.
 (* case 3.2.5: n >= i *)
       EApply ty0_abbr; XEAuto.
-(* case 3.3: fsubst0_b *)
+(* case 3.3: fsubst0_both *)
       Subst0GenBase; Rewrite H7; Rewrite <- H3 in H4; Rewrite <- H3 in H6; Clear H3 H7 i t3.
       DropDis; Inversion H6; Rewrite <- H7 in H0; Rewrite H8 in H1.
       CSubst0Drop; XEAuto.
 (* case 4: ty0_abst *)
       Intros until 5; XElim H3; Intros; Clear c1 c2 t t1 t2.
-(* case 4.1: fsubst0_t *)
+(* case 4.1: fsubst0_snd *)
       Subst0GenBase; Rewrite H3 in H0; DropDis; Inversion H0.
-(* case 4.2: fsubst0_c *)
+(* case 4.2: fsubst0_fst *)
       Apply (lt_le_e n i); Intros; CSubst0Drop.
 (* case 4.2.1: n < i, none *)
       EApply ty0_abst; XEAuto.
-(* case 4.2.2: n < i, csubst0_fst *)
+(* case 4.2.2: n < i, csubst0_snd *)
       Inversion H0; CSubst0Drop.
       Rewrite <- H10 in H7; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H8; Rewrite <- H12;
       Clear H0 H10 H11 H12 x0 x1 x2.
       DropDis; Rewrite minus_x_Sy in H0; [ DropGenBase | XAuto ].
       IHT; EApply ty0_conv;
       [ EApply ty0_lift | EApply ty0_abst | EApply pc3_lift ]; XEAuto.
-(* case 4.2.3: n < i, csubst0_snd *)
+(* case 4.2.3: n < i, csubst0_fst *)
       Inversion H0; CSubst0Drop.
       Rewrite <- H10 in H8; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H7; Rewrite <- H12;
       Clear H0 H10 H11 H12 x0 x1 x3.
@@ -207,11 +209,11 @@ Require ty0_props.
       ]; XEAuto.
 (* case 4.2.4: n >= i *)
       EApply ty0_abst; XEAuto.
-(* case 4.3: fsubst0_b *)
+(* case 4.3: fsubst0_both *)
       Subst0GenBase; Rewrite H3 in H0; DropDis; Inversion H0.
 (* case 5: ty0_bind *)
       Intros until 7; XElim H5; Intros; Clear H4.
-(* case 5.1: fsubst0_t *)
+(* case 5.1: fsubst0_snd *)
       Subst0GenBase; Rewrite H4; Clear H4 t6.
 (* case 5.1.1: subst0 on left argument *)
       Ty0Correct; IHT; IHTb1; Ty0Correct.
@@ -223,9 +225,9 @@ Require ty0_props.
       Ty0Correct; IHT; IHTb1; IHTTb; Ty0Correct.
       EApply ty0_conv;
       [ EApply ty0_bind | EApply ty0_bind | EApply pc3_fsubst0 ]; XEAuto.
-(* case 5.2: fsubst0_c *)
+(* case 5.2: fsubst0_fst *)
       IHC; IHCb; Ty0Correct; EApply ty0_bind; XEAuto.
-(* case 5.3: fsubst0_b *)
+(* case 5.3: fsubst0_both *)
       Subst0GenBase; Rewrite H4; Clear H4 t6.
 (* case 5.3.1: subst0 on left argument *)
       IHC; IHCb; Ty0Correct; Ty0Correct; IHCT; IHCTb1; Ty0Correct.
@@ -241,7 +243,7 @@ Require ty0_props.
       | EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
 (* case 6: ty0_appl *)
       Intros until 5; XElim H3; Intros.
-(* case 6.1: fsubst0_t *)
+(* case 6.1: fsubst0_snd *)
       Subst0GenBase; Rewrite H3; Clear H3 c1 c2 t t1 t2 t3.
 (* case 6.1.1: subst0 on left argument *)
       Ty0Correct; Ty0GenBase; IHT; Ty0Correct.
@@ -253,9 +255,9 @@ Require ty0_props.
       Ty0Correct; Ty0GenBase; Move H after H10; Ty0Correct; IHT; Clear H2; IHT.
       EApply ty0_conv;
       [ EApply ty0_appl | EApply ty0_appl | EApply pc3_fsubst0 ]; XEAuto.
-(* case 6.2: fsubst0_c *)
+(* case 6.2: fsubst0_fst *)
       IHC; Clear H2; IHC; EApply ty0_appl; XEAuto.
-(* case 6.3: fsubst0_b *)
+(* case 6.3: fsubst0_both *)
       Subst0GenBase; Rewrite H3; Clear H3 c1 c2 t t1 t2 t3.
 (* case 6.3.1: subst0 on left argument *)
       IHC; Ty0Correct; Ty0GenBase; Clear H2; IHC; IHCT.
@@ -271,7 +273,7 @@ Require ty0_props.
       | EApply pc3_fsubst0; [ Idtac | Idtac | XEAuto ] ]; XEAuto.
 (* case 7: ty0_cast *)
       Clear c1 t t1; Intros until 5; XElim H3; Intros; Clear c2 t3.
-(* case 7.1: fsubst0_t *)
+(* case 7.1: fsubst0_snd *)
       Subst0GenBase; Rewrite H3; Clear H3 t4.
 (* case 7.1.1: subst0 on left argument *)
       IHT; EApply ty0_conv;
@@ -290,9 +292,9 @@ Require ty0_props.
         [ EApply ty0_conv; [ Idtac | Idtac | Apply pc3_s; EApply pc3_fsubst0 ]
         | Idtac ]
       | EApply pc3_fsubst0 ]; XEAuto.
-(* case 7.2: fsubst0_c *)
+(* case 7.2: fsubst0_fst *)
       IHC; Clear H2; IHC; EApply ty0_cast; XEAuto.
-(* case 6.3: fsubst0_b *)
+(* case 6.3: fsubst0_both *)
       Subst0GenBase; Rewrite H3; Clear H3 t4.
 (* case 7.3.1: subst0 on left argument *)
       IHC; IHCT; Clear H2; IHC.
@@ -330,4 +332,3 @@ Require ty0_props.
    End ty0_fsubst0.
 
       Hints Resolve ty0_subst0 : ltlc.
-