X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fcsubt%2Fpc3.ma;h=d8a6ad246a78b8ff470fdb23d81bb13be6ca2744;hb=b58315ef220a130a44acbf528cd6885ddadad642;hp=86a83b5e727ee576c2db986504eb2f6d4e7d991d;hpb=354c363760b5d5222b82674fca38e9c0dc55010e;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/pc3.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/pc3.ma
index 86a83b5e7..d8a6ad246 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/pc3.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/pc3.ma
@@ -49,9 +49,9 @@ T).(\lambda (c2: C).(\lambda (_: (csubt g c1 c2)).(pc3_refl c2 t)))) (\lambda
 (t0: T).(\lambda (t3: T).(\lambda (H0: (pr2 c1 t0 t3)).(\lambda (t4: 
 T).(\lambda (_: (pc3 c1 t3 t4)).(\lambda (H2: ((\forall (c2: C).((csubt g c1 
 c2) \to (pc3 c2 t3 t4))))).(\lambda (c2: C).(\lambda (H3: (csubt g c1 
-c2)).(pc3_pr2_u c2 t3 t0 (csubt_pr2 g c1 t0 t3 H0 c2 H3) t4 (H2 c2 
-H3)))))))))) (\lambda (t0: T).(\lambda (t3: T).(\lambda (H0: (pr2 c1 t0 
-t3)).(\lambda (t4: T).(\lambda (_: (pc3 c1 t0 t4)).(\lambda (H2: ((\forall 
+c2)).(pc3_t t3 c2 t0 (pc3_pr2_r c2 t0 t3 (csubt_pr2 g c1 t0 t3 H0 c2 H3)) t4 
+(H2 c2 H3)))))))))) (\lambda (t0: T).(\lambda (t3: T).(\lambda (H0: (pr2 c1 
+t0 t3)).(\lambda (t4: T).(\lambda (_: (pc3 c1 t0 t4)).(\lambda (H2: ((\forall 
 (c2: C).((csubt g c1 c2) \to (pc3 c2 t0 t4))))).(\lambda (c2: C).(\lambda 
 (H3: (csubt g c1 c2)).(pc3_t t0 c2 t3 (pc3_pr2_x c2 t3 t0 (csubt_pr2 g c1 t0 
 t3 H0 c2 H3)) t4 (H2 c2 H3)))))))))) t1 t2 H))))).