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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/ty0_gen_context.v b/helm/coq-contribs/LAMBDA-TYPES/ty0_gen_context.v
index bf9217602..3a5b5d9b7 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/ty0_gen_context.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/ty0_gen_context.v
@@ -35,14 +35,14 @@ Require ty0_lift.
                                          (ty0 g a y1 y2)
                              ).
       Intros until 1; XElim H; Intros.
-(* case 1 : ty0_conv *)
+(* case 1: ty0_conv *)
       Repeat IH d a0 a; EApply ex3_2_intro;
       [ XEAuto | XEAuto | EApply ty0_conv; Try EApply pc3_gen_cabbr; XEAuto ].
-(* case 2 : ty0_sort *)
+(* case 2: ty0_sort *)
       EApply ex3_2_intro; Try Rewrite lift_sort; XAuto.
-(* case 3 : ty0_abbr *)
+(* case 3: ty0_abbr *)
       Apply (lt_eq_gt_e n d0); Intros; Clear c t1 t2.
-(* case 3.1 : n < d0 *)
+(* case 3.1: n < d0 *)
       Clear H1; DropDis; Rewrite minus_x_Sy in H1; [ DropGenBase | XAuto ].
       CSubst1Drop; Rewrite minus_x_Sy in H0; [ Idtac | XAuto ].
       CSubst1GenBase; Rewrite H0 in H8; Clear H0 x; Simpl in H9.
@@ -53,8 +53,8 @@ Require ty0_lift.
       Pattern 3 d0; Rewrite (le_plus_minus_sym (S n) d0); [ Idtac | XAuto ].
       Pattern 4 d0; Rewrite (le_plus_minus (S n) d0); [ Idtac | XAuto ].
       EApply ex3_2_intro;
-      [ Rewrite lift_bref_lt | Rewrite lift_d | EApply ty0_abbr ]; XEAuto.
-(* case 3.2 : n = d0 *)
+      [ Rewrite lift_lref_lt | Rewrite lift_d | EApply ty0_abbr ]; XEAuto.
+(* case 3.2: n = d0 *)
       Rewrite H7; Rewrite H7 in H0; Clear H2 H7 n.
       DropDis; Inversion H0; Rewrite H8 in H4; Clear H0 H7 H8 e u0.
       CSubst1Drop; DropDis.
@@ -62,18 +62,18 @@ Require ty0_lift.
       [ EApply subst1_single; Rewrite lift_free; Simpl; XEAuto
       | Rewrite lift_free; Simpl; XEAuto
       | XEAuto ].
-(* case 3.3 : n > d0 *)
+(* case 3.3: n > d0 *)
       Clear H2 H3 e; CSubst1Drop; DropDis.
       Pattern 1 n; Rewrite (lt_plus_minus (0) n); [ Idtac | XEAuto ].
       Arith4c '(0) '(minus n (1)).
       EApply ex3_2_intro;
-      [ Rewrite lift_bref_ge
+      [ Rewrite lift_lref_ge
       | Rewrite lift_free; Simpl
       | Pattern 2 n; Rewrite (minus_x_SO n)
       ]; XEAuto.
-(* case 4 : ty0_abst *)
+(* case 4: ty0_abst *)
       Apply (lt_eq_gt_e n d0); Intros; Clear c t1 t2.
-(* case 4.1 : n < d0 *)
+(* case 4.1: n < d0 *)
       Clear H1; DropDis; Rewrite minus_x_Sy in H1; [ DropGenBase | XAuto ].
       CSubst1Drop; Rewrite minus_x_Sy in H0; [ Idtac | XAuto ].
       CSubst1GenBase; Rewrite H0 in H8; Clear H0 x; Simpl in H9.
@@ -84,31 +84,31 @@ Require ty0_lift.
       Pattern 3 d0; Rewrite (le_plus_minus_sym (S n) d0); [ Idtac | XAuto ].
       Pattern 4 d0; Rewrite (le_plus_minus (S n) d0); [ Idtac | XAuto ].
       EApply ex3_2_intro;
-      [ Rewrite lift_bref_lt | Rewrite lift_d | EApply ty0_abst ]; XEAuto.
-(* case 4.2 : n = d0 *)
+      [ Rewrite lift_lref_lt | Rewrite lift_d | EApply ty0_abst ]; XEAuto.
+(* case 4.2: n = d0 *)
       Rewrite H7; Rewrite H7 in H0; DropDis; Inversion H0.
-(* case 4.3 : n > d0 *)
+(* case 4.3: n > d0 *)
       Clear H2 H3 e; CSubst1Drop; DropDis.
       Pattern 1 n; Rewrite (lt_plus_minus (0) n); [ Idtac | XEAuto ].
       Arith4c '(0) '(minus n (1)).
       EApply ex3_2_intro;
-      [ Rewrite lift_bref_ge
+      [ Rewrite lift_lref_ge
       | Rewrite lift_free; Simpl
       | Pattern 2 n; Rewrite (minus_x_SO n)
       ]; XEAuto.
-(* case 5 : ty0_bind *)
+(* case 5: ty0_bind *)
       IH d a0 a; Clear H H1 H3 c t1 t2.
       IH '(S d) '(CTail a0 (Bind b) (lift (1) d x0)) '(CTail a (Bind b) x0).
       IH '(S d) '(CTail a0 (Bind b) (lift (1) d x0)) '(CTail a (Bind b) x0).
       Subst1Confluence; Rewrite H4 in H11; Clear H4 x5.
       EApply ex3_2_intro; Try Rewrite lift_bind; XEAuto.
-(* case 6 : ty0_appl *)
+(* case 6: ty0_appl *)
       Repeat IH d a0 a; Clear H H1 c t1 t2.
       Subst1GenBase; SymEqual; LiftGenBase; Rewrite H in H8; Rewrite H11 in H1; Rewrite H12 in H7; Clear H H11 H12 x1 x4 x5.
       Subst1Confluence; Rewrite H in H8; Clear H x6.
       EApply ex3_2_intro; Try Rewrite lift_flat;
       [ Idtac | EApply subst1_tail; [ Idtac | Rewrite lift_bind ] | Idtac ]; XEAuto.
-(* case 7 : ty0_cast *)
+(* case 7: ty0_cast *)
       Rename u into u0; Repeat IH d a0 a; Clear H H1 c t1 t2.
       Subst1Confluence; Rewrite H in H10; Clear H x3.
       EApply ex3_2_intro; [ Rewrite lift_flat | Idtac | Idtac ]; XEAuto.
@@ -135,13 +135,13 @@ Require ty0_lift.
                                          (ty0 g a y1 y2)
                              ).
       Intros until 1; XElim H; Intros.
-(* case 1 : ty0_conv *)
+(* case 1: ty0_conv *)
       Repeat IH d a; Rewrite H0 in H3; Rewrite H7 in H3; Pc3Gen; XEAuto.
-(* case 2 : ty0_sort *)
+(* case 2: ty0_sort *)
       EApply ex3_2_intro; Try Rewrite lift_sort; XEAuto.
-(* case 3 : ty0_abbr *)
+(* case 3: ty0_abbr *)
       Apply (lt_eq_gt_e n d0); Intros.
-(* case 3.1 : n < d0 *)
+(* case 3.1: n < d0 *)
       DropDis; Rewrite minus_x_Sy in H7; [ DropGenBase | XAuto ].
       Rewrite (lt_plus_minus n d0) in H5; [ Idtac | XAuto ].
       DropDis; Rewrite H0 in H2; Clear H0 H1 u.
@@ -149,21 +149,21 @@ Require ty0_lift.
       LiftGen; Rewrite <- H0 in H2; Clear H0 x2.
       Rewrite <- lift_d; [ Idtac | XAuto ].
       Rewrite <- le_plus_minus; [ Idtac | XAuto ].
-      EApply ex3_2_intro; [ Rewrite lift_bref_lt | Idtac | EApply ty0_abbr ]; XEAuto.
-(* case 3.2 : n = d0 *)
+      EApply ex3_2_intro; [ Rewrite lift_lref_lt | Idtac | EApply ty0_abbr ]; XEAuto.
+(* case 3.2: n = d0 *)
       Rewrite H6 in H0; DropDis; Inversion H0.
-(* case 3.3 : n > d0 *)
+(* case 3.3: n > d0 *)
       Clear H2 H3 c e t1 t2 u0; DropDis.
       Pattern 1 n; Rewrite (lt_plus_minus (0) n); [ Idtac | XEAuto ].
       Arith4c '(0) '(minus n (1)).
       EApply ex3_2_intro;
-      [ Rewrite lift_bref_ge
+      [ Rewrite lift_lref_ge
       | Rewrite lift_free; Simpl
       | Pattern 2 n; Rewrite (minus_x_SO n)
       ]; XEAuto.
-(* case 4 : ty0_abst *)
+(* case 4: ty0_abst *)
       Apply (lt_eq_gt_e n d0); Intros.
-(* case 4.1 : n < d0 *)
+(* case 4.1: n < d0 *)
       DropDis; Rewrite minus_x_Sy in H7; [ DropGenBase | XAuto ].
       Rewrite (lt_plus_minus n d0) in H5; [ Idtac | XAuto ].
       DropDis; Rewrite H0; Rewrite H0 in H2; Clear H0 H1 u.
@@ -171,31 +171,31 @@ Require ty0_lift.
       LiftGen; Rewrite <- H0 in H2; Clear H0 x2.
       Rewrite <- lift_d; [ Idtac | XAuto ].
       Rewrite <- le_plus_minus; [ Idtac | XAuto ].
-      EApply ex3_2_intro; [ Rewrite lift_bref_lt | Idtac | EApply ty0_abst ]; XEAuto.
-(* case 4.2 : n = d0 *)
+      EApply ex3_2_intro; [ Rewrite lift_lref_lt | Idtac | EApply ty0_abst ]; XEAuto.
+(* case 4.2: n = d0 *)
       Rewrite H6 in H0; DropDis; Inversion H0.
-(* case 4.3 : n > d0 *)
+(* case 4.3: n > d0 *)
       Clear H2 H3 c e t1 t2 u0; DropDis.
       Pattern 1 n; Rewrite (lt_plus_minus (0) n); [ Idtac | XEAuto ].
       Arith4c '(0) '(minus n (1)).
       EApply ex3_2_intro;
-      [ Rewrite lift_bref_ge
+      [ Rewrite lift_lref_ge
       | Rewrite lift_free; [ Simpl | Simpl | Idtac ]
       | Pattern 2 n; Rewrite (minus_x_SO n)
       ]; XEAuto.
-(* case 5 : ty0_bind *)
+(* case 5: ty0_bind *)
       IH d a; Rewrite H0; Rewrite H0 in H2; Rewrite H0 in H4; Clear H H0 H1 H3 H8 u t.
       IH '(S d) '(CTail a (Bind b) x0); Rewrite H; Rewrite H in H2; Clear H H0 t3 t4.
       IH '(S d) '(CTail a (Bind b) x0); Rewrite H; Clear H t0.
       LiftGen; Rewrite <- H in H2; Clear H x5.
       LiftTailRwBack; XEAuto.
-(* case 6 : ty0_appl *)
+(* case 6: ty0_appl *)
       IH d a; Rewrite H2; Clear H H1 H2 v.
       LiftGenBase; Rewrite H in H7; Rewrite H1; Rewrite H1 in H0; Rewrite H2; Clear H H1 H2 u t x1.
       IH d a; Rewrite H; Clear H w.
       LiftGen; Rewrite <- H in H1; Clear H x4.
       LiftTailRwBack; XEAuto.
-(* case 7 : ty0_cast *)
+(* case 7: ty0_cast *)
       Rename u into u0.
       IH d a; Rewrite H2 in H0; Rewrite H2; Clear H H1 H2 H6 t3 t4.
       IH d a; Rewrite H; Clear H t0.