X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fty0_sred.v;h=99548beb5220547332feb751a85908151a6c69e5;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=62aa5c3993a1b7d24e20eb59620fe0edf2c412fc;hpb=50cfabb6b8136873a02f8fd1512f0b62f97e2639;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/ty0_sred.v b/helm/coq-contribs/LAMBDA-TYPES/ty0_sred.v
index 62aa5c399..99548beb5 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/ty0_sred.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/ty0_sred.v
@@ -4,14 +4,17 @@ Require csubst1_defs.
 Require pr0_lift.
 Require pr0_subst1.
 Require cpr0_defs.
+Require pc1_props.
 Require pc3_props.
 Require pc3_gen.
 Require ty0_defs.
+Require ty0_gen.
 Require ty0_lift.
 Require ty0_props.
 Require ty0_subst0.
 Require ty0_gen_context.
 Require csub0_defs.
+Require csub0_props.
 
 (*#* #caption "subject reduction" #clauses *)
 
@@ -178,7 +181,7 @@ Require csub0_defs.
         ]; XEAuto
       | Idtac ].
       Rewrite <- lift_bind; Apply pc3_pc1;
-      Apply (pc1_u (TTail (Flat Appl) v2 (TTail (Bind b) u2 (lift (1) (0) (TTail (Bind Abst) u t0))))); XAuto.
+      Apply (pc1_pr0_u2 (TTail (Flat Appl) v2 (TTail (Bind b) u2 (lift (1) (0) (TTail (Bind Abst) u t0))))); XAuto.
 (* case 7: ty0_cast *)
       Intros; Inversion H5; Clear H5.
 (* case 7.1: pr0_refl *)
@@ -220,7 +223,7 @@ Require csub0_defs.
 
 (*#* #start file *)
 
-(*#* #caption "general case" *)
+(*#* #caption "general case without the reduction in the context" *)
 (*#* #cap #cap c #alpha t1 in T, t2 in T1, t in T2 *)
 
       Theorem ty0_sred_pr3: (c:?; t1,t2:?) (pr3 c t1 t2) ->