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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr2_gen_context.v b/helm/coq-contribs/LAMBDA-TYPES/pr2_gen_context.v
index b2cfaead1..61d2ffef7 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/pr2_gen_context.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/pr2_gen_context.v
@@ -8,6 +8,7 @@ Require csubst1_defs.
 Require pr0_gen.
 Require pr0_subst1.
 Require pr2_defs.
+Require pr2_gen.
 Require pr2_subst1.
 
    Section pr2_gen_context. (************************************************)
@@ -20,27 +21,29 @@ Require pr2_subst1.
                              (EX x2 | (subst1 d u t2 (lift (1) d x2)) &
                                       (pr2 a x1 x2)
                              ).
-      Intros until 1; XElim H; Intros.
-(* case 1: pr2_pr0 *)
-      Pr0Subst1; Pr0Gen; Rewrite H in H3; Clear H x; XEAuto.
+      Intros until 1; XElim H; Intros;
+      Pr0Subst1; Pr0Gen.
+(* case 1: pr2_free *)
+      Rewrite H in H3; Clear H x; XEAuto.
 (* case 2: pr2_delta *)
+      Rewrite H0 in H5; Clear H0 x.  
       Apply (lt_eq_gt_e i d0); Intros.
 (* case 2.1: i < d0 *)
       Subst1Confluence; CSubst1Drop.
       Rewrite minus_x_Sy in H; [ Idtac | XAuto ].
-      CSubst1GenBase; Rewrite H in H6; Clear H x0.
-      Rewrite (lt_plus_minus i d0) in H3; [ Idtac | XAuto ].
-      DropDis; Rewrite H in H7; Clear H x2.
+      CSubst1GenBase; Rewrite H in H7; Clear H x2.
+      Rewrite (lt_plus_minus i d0) in H4; [ Idtac | XAuto ].
+      DropDis; Rewrite H in H8; Clear H x3.
       Subst1Subst1; Pattern 2 d0 in H; Rewrite (lt_plus_minus i d0) in H; [ Idtac | XAuto ].
-      Subst1Gen; Rewrite H in H9; Simpl in H9; Clear H x2.
-      Rewrite <- lt_plus_minus in H9; [ Idtac | XAuto ].
-      Rewrite <- lt_plus_minus_r in H9; XEAuto.
+      Subst1Gen; Rewrite H in H10; Simpl in H10; Clear H x3.
+      Rewrite <- lt_plus_minus in H10; [ Idtac | XAuto ].
+      Rewrite <- lt_plus_minus_r in H10; XEAuto.
 (* case 2.2: i = d0 *)
-      Rewrite H5 in H; Rewrite H5 in H0; Clear H5 i.
-      DropDis; Inversion H; Rewrite <- H7 in H0; Rewrite <- H7 in H1; Rewrite <- H7; Clear H H6 H7 e u.
+      Rewrite H0 in H; Rewrite H0 in H1; Clear H0 i.
+      DropDis; Inversion H; Rewrite <- H8 in H1; Rewrite <- H8 in H2; Rewrite <- H8; Clear H H7 H8 e u.
       Subst1Confluence; Subst1Gen; Rewrite H0 in H; Clear H0 x; XEAuto.
 (* case 2.3: i > d0 *)
-      Subst1Confluence; Subst1Gen; Rewrite H4 in H0; Clear H1 H4 x.
+      Subst1Confluence; Subst1Gen; Rewrite H5 in H1; Clear H2 H5 x.
       CSubst1Drop; DropDis; XEAuto.
       Qed.