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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/lift_gen.v b/helm/coq-contribs/LAMBDA-TYPES/lift_gen.v
index 14914d4cb..63b74709d 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/lift_gen.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/lift_gen.v
@@ -11,26 +11,21 @@ Require lift_defs.
             | [ H1: (lift ?1 ?2 t0) = (lift ?1 ?2 ?3) |- ? ] ->
                LApply (H0 ?3 ?1 ?2); [ Clear H0 H1; Intros | XAuto ].
 
-(*#* #start file *)
-
 (*#* #caption "main properties of lift" #clauses lift_props *)
 
 (*#* #caption "injectivity" *)
 (*#* #cap #alpha x in T1, t in T2, d in i *)
 
       Theorem lift_inj : (x,t:?; h,d:?) (lift h d x) = (lift h d t) -> x = t.
-
-(*#* #stop file *)
-
       XElim x.
 (* case 1 : TSort *)
       Intros; Rewrite lift_sort in H; LiftGenBase; XAuto.
-(* case 2 : TBRef n *)
+(* case 2 : TLRef n *)
       Intros; Apply (lt_le_e n d); Intros.
 (* case 2.1 : n < d *)
-      Rewrite lift_bref_lt in H; [ LiftGenBase; XAuto | XAuto ].
+      Rewrite lift_lref_lt in H; [ LiftGenBase; XAuto | XAuto ].
 (* case 2.2 : n >= d *)
-      Rewrite lift_bref_ge in H; [ LiftGenBase; XAuto | XAuto ].
+      Rewrite lift_lref_ge in H; [ LiftGenBase; XAuto | XAuto ].
 (* case 3 : TTail k *)
       XElim k; Intros; [ Rewrite lift_bind in H1 | Rewrite lift_flat in H1 ];
       LiftGenBase; Rewrite H1; IH; IH; XAuto.
@@ -51,8 +46,6 @@ Require lift_defs.
                LApply H0; [ Clear H0 H_x; Intros H0 | XAuto ];
                XElim H0; Intros.
 
-(*#* #start file *)
-
 (*#* #caption "generation lemma for lift" *)
 (*#* #cap #cap t1 #alpha t2 in T, x in T2, d1 in i1, d2 in i2 *)
 
@@ -61,30 +54,27 @@ Require lift_defs.
                               (EX t2 | x = (lift h1 d1 t2) &
                                        t1 = (lift h2 d2 t2)
                               ).
-
-(*#* #stop file *)
-
       XElim t1; Intros.
 (* case 1 : TSort *)
       Rewrite lift_sort in H0.
       LiftGenBase; Rewrite H0; Clear H0 x.
       EApply ex2_intro; Rewrite lift_sort; XAuto.
-(* case 2 : TBRef n *)
+(* case 2 : TLRef n *)
       Apply (lt_le_e n d1); Intros.
 (* case 2.1 : n < d1 *)
-      Rewrite lift_bref_lt in H0; [ Idtac | XAuto ].
+      Rewrite lift_lref_lt in H0; [ Idtac | XAuto ].
       LiftGenBase; Rewrite H0; Clear H0 x.
-      EApply ex2_intro; Rewrite lift_bref_lt; XEAuto.
+      EApply ex2_intro; Rewrite lift_lref_lt; XEAuto.
 (* case 2.2 : n >= d1 *)
-      Rewrite lift_bref_ge in H0; [ Idtac | XAuto ].
+      Rewrite lift_lref_ge in H0; [ Idtac | XAuto ].
       Apply (lt_le_e n d2); Intros.
 (* case 2.2.1 : n < d2 *)
       LiftGenBase; Rewrite H0; Clear H0 x.
-      EApply ex2_intro; [ Rewrite lift_bref_ge | Rewrite lift_bref_lt ]; XEAuto.
+      EApply ex2_intro; [ Rewrite lift_lref_ge | Rewrite lift_lref_lt ]; XEAuto.
 (* case 2.2.2 : n >= d2 *)
       Apply (lt_le_e n (plus d2 h2)); Intros.
 (* case 2.2.2.1 : n < d2 + h2 *)
-      EApply lift_gen_bref_false; [ Idtac | Idtac | Apply H0 ];
+      EApply lift_gen_lref_false; [ Idtac | Idtac | Apply H0 ];
       [ XAuto | Rewrite plus_permute_2_in_3; XAuto ].
 (* case 2.2.2.2 : n >= d2 + h2 *)
       Rewrite (le_plus_minus_sym h2 (plus n h1)) in H0; [ Idtac | XEAuto ].
@@ -92,7 +82,7 @@ Require lift_defs.
       EApply ex2_intro;
       [ Rewrite le_minus_plus; [ Idtac | XEAuto ]
       | Rewrite (le_plus_minus_sym h2 n); [ Idtac | XEAuto ] ];
-      Rewrite lift_bref_ge; XEAuto.
+      Rewrite lift_lref_ge; XEAuto.
 (* case 3 : TTail k *)
       NewInduction k.
 (* case 3.1 : Bind *)