X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fcsubc%2Fcsuba.ma;h=73f8956e4617c8c670230d4d98fc347b10082b04;hb=f73bd1c1cdd504c2a991071505b2e4f541791a7f;hp=c4a7269fbebf4558789f082c2a0ee4d8163a2959;hpb=5c1b44dfefa085fbb56e23047652d3650be9d855;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/csuba.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/csuba.ma
index c4a7269fb..73f8956e4 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/csuba.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/csuba.ma
@@ -14,13 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
+include "LambdaDelta-1/csubc/defs.ma".
 
-
-include "csubc/defs.ma".
-
-include "sc3/props.ma".
-
-include "csuba/defs.ma".
+include "LambdaDelta-1/sc3/props.ma".
 
 theorem csubc_csuba:
  \forall (g: G).(\forall (c1: C).(\forall (c2: C).((csubc g c1 c2) \to (csuba 
@@ -31,6 +27,9 @@ c2)).(csubc_ind g (\lambda (c: C).(\lambda (c0: C).(csuba g c c0))) (\lambda
 (n: nat).(csuba_refl g (CSort n))) (\lambda (c3: C).(\lambda (c4: C).(\lambda 
 (_: (csubc g c3 c4)).(\lambda (H1: (csuba g c3 c4)).(\lambda (k: K).(\lambda 
 (v: T).(csuba_head g c3 c4 H1 k v))))))) (\lambda (c3: C).(\lambda (c4: 
+C).(\lambda (_: (csubc g c3 c4)).(\lambda (H1: (csuba g c3 c4)).(\lambda (b: 
+B).(\lambda (H2: (not (eq B b Void))).(\lambda (u1: T).(\lambda (u2: 
+T).(csuba_void g c3 c4 H1 b H2 u1 u2))))))))) (\lambda (c3: C).(\lambda (c4: 
 C).(\lambda (_: (csubc g c3 c4)).(\lambda (H1: (csuba g c3 c4)).(\lambda (v: 
 T).(\lambda (a: A).(\lambda (H2: (sc3 g (asucc g a) c3 v)).(\lambda (w: 
 T).(\lambda (H3: (sc3 g a c4 w)).(csuba_abst g c3 c4 H1 v a (sc3_arity_gen g