X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fcsubt%2Fty3.ma;h=6334713f61dcf432208b991cf6bb9a9dff107028;hb=f5dfc6c24a393a4717a7b40689df768d271d9ac0;hp=23677feed32d7540a242d398c22a542e4d84aff7;hpb=5c1b44dfefa085fbb56e23047652d3650be9d855;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/ty3.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/ty3.ma
index 23677feed..6334713f6 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/ty3.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/ty3.ma
@@ -14,11 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
+include "LambdaDelta-1/csubt/pc3.ma".
 
-
-include "csubt/pc3.ma".
-
-include "csubt/props.ma".
+include "LambdaDelta-1/csubt/props.ma".
 
 theorem csubt_ty3:
  \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (t2: T).((ty3 g c1 
@@ -70,16 +68,13 @@ T).(\lambda (_: (ty3 g c u t)).(\lambda (H1: ((\forall (c2: C).((csubt g c
 c2) \to (ty3 g c2 u t))))).(\lambda (b: B).(\lambda (t0: T).(\lambda (t3: 
 T).(\lambda (_: (ty3 g (CHead c (Bind b) u) t0 t3)).(\lambda (H3: ((\forall 
 (c2: C).((csubt g (CHead c (Bind b) u) c2) \to (ty3 g c2 t0 t3))))).(\lambda 
-(t4: T).(\lambda (_: (ty3 g (CHead c (Bind b) u) t3 t4)).(\lambda (H5: 
-((\forall (c2: C).((csubt g (CHead c (Bind b) u) c2) \to (ty3 g c2 t3 
-t4))))).(\lambda (c2: C).(\lambda (H6: (csubt g c c2)).(ty3_bind g c2 u t (H1 
-c2 H6) b t0 t3 (H3 (CHead c2 (Bind b) u) (csubt_head g c c2 H6 (Bind b) u)) 
-t4 (H5 (CHead c2 (Bind b) u) (csubt_head g c c2 H6 (Bind b) 
-u)))))))))))))))))) (\lambda (c: C).(\lambda (w: T).(\lambda (u: T).(\lambda 
-(_: (ty3 g c w u)).(\lambda (H1: ((\forall (c2: C).((csubt g c c2) \to (ty3 g 
-c2 w u))))).(\lambda (v: T).(\lambda (t: T).(\lambda (_: (ty3 g c v (THead 
-(Bind Abst) u t))).(\lambda (H3: ((\forall (c2: C).((csubt g c c2) \to (ty3 g 
-c2 v (THead (Bind Abst) u t)))))).(\lambda (c2: C).(\lambda (H4: (csubt g c 
+(c2: C).(\lambda (H4: (csubt g c c2)).(ty3_bind g c2 u t (H1 c2 H4) b t0 t3 
+(H3 (CHead c2 (Bind b) u) (csubt_head g c c2 H4 (Bind b) u))))))))))))))) 
+(\lambda (c: C).(\lambda (w: T).(\lambda (u: T).(\lambda (_: (ty3 g c w 
+u)).(\lambda (H1: ((\forall (c2: C).((csubt g c c2) \to (ty3 g c2 w 
+u))))).(\lambda (v: T).(\lambda (t: T).(\lambda (_: (ty3 g c v (THead (Bind 
+Abst) u t))).(\lambda (H3: ((\forall (c2: C).((csubt g c c2) \to (ty3 g c2 v 
+(THead (Bind Abst) u t)))))).(\lambda (c2: C).(\lambda (H4: (csubt g c 
 c2)).(ty3_appl g c2 w u (H1 c2 H4) v t (H3 c2 H4))))))))))))) (\lambda (c: 
 C).(\lambda (t0: T).(\lambda (t3: T).(\lambda (_: (ty3 g c t0 t3)).(\lambda 
 (H1: ((\forall (c2: C).((csubt g c c2) \to (ty3 g c2 t0 t3))))).(\lambda (t4: