X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fcsuba%2Fclear.ma;h=83977c438ff5fb6efa54016cdc8d7f42a65b5229;hb=f73bd1c1cdd504c2a991071505b2e4f541791a7f;hp=036ca2882f24e9251e0946433362e02356096112;hpb=831af787465e1bff886e22ee14b68c8f1bb0177c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/clear.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/clear.ma
index 036ca2882..83977c438 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/clear.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/clear.ma
@@ -14,11 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csuba/clear".
+include "LambdaDelta-1/csuba/defs.ma".
 
-include "csuba/defs.ma".
-
-include "clear/fwd.ma".
+include "LambdaDelta-1/clear/fwd.ma".
 
 theorem csuba_clear_conf:
  \forall (g: G).(\forall (c1: C).(\forall (c2: C).((csuba g c1 c2) \to 
@@ -51,8 +49,18 @@ C).(\lambda (H5: (csuba g e1 x)).(\lambda (H6: (clear c4 x)).(ex_intro2 C
 u) e2)) x H5 (clear_flat c4 x H6 f u))))) H4)))) k H2))))))))) (\lambda (c3: 
 C).(\lambda (c4: C).(\lambda (H0: (csuba g c3 c4)).(\lambda (_: ((\forall 
 (e1: C).((clear c3 e1) \to (ex2 C (\lambda (e2: C).(csuba g e1 e2)) (\lambda 
-(e2: C).(clear c4 e2))))))).(\lambda (t: T).(\lambda (a: A).(\lambda (H2: 
-(arity g c3 t (asucc g a))).(\lambda (u: T).(\lambda (H3: (arity g c4 u 
+(e2: C).(clear c4 e2))))))).(\lambda (b: B).(\lambda (H2: (not (eq B b 
+Void))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (e1: C).(\lambda (H3: 
+(clear (CHead c3 (Bind Void) u1) e1)).(eq_ind_r C (CHead c3 (Bind Void) u1) 
+(\lambda (c: C).(ex2 C (\lambda (e2: C).(csuba g c e2)) (\lambda (e2: 
+C).(clear (CHead c4 (Bind b) u2) e2)))) (ex_intro2 C (\lambda (e2: C).(csuba 
+g (CHead c3 (Bind Void) u1) e2)) (\lambda (e2: C).(clear (CHead c4 (Bind b) 
+u2) e2)) (CHead c4 (Bind b) u2) (csuba_void g c3 c4 H0 b H2 u1 u2) 
+(clear_bind b c4 u2)) e1 (clear_gen_bind Void c3 e1 u1 H3)))))))))))) 
+(\lambda (c3: C).(\lambda (c4: C).(\lambda (H0: (csuba g c3 c4)).(\lambda (_: 
+((\forall (e1: C).((clear c3 e1) \to (ex2 C (\lambda (e2: C).(csuba g e1 e2)) 
+(\lambda (e2: C).(clear c4 e2))))))).(\lambda (t: T).(\lambda (a: A).(\lambda 
+(H2: (arity g c3 t (asucc g a))).(\lambda (u: T).(\lambda (H3: (arity g c4 u 
 a)).(\lambda (e1: C).(\lambda (H4: (clear (CHead c3 (Bind Abst) t) 
 e1)).(eq_ind_r C (CHead c3 (Bind Abst) t) (\lambda (c: C).(ex2 C (\lambda 
 (e2: C).(csuba g c e2)) (\lambda (e2: C).(clear (CHead c4 (Bind Abbr) u) 
@@ -92,8 +100,18 @@ C).(\lambda (H5: (csuba g x e1)).(\lambda (H6: (clear c3 x)).(ex_intro2 C
 u) e2)) x H5 (clear_flat c3 x H6 f u))))) H4)))) k H2))))))))) (\lambda (c3: 
 C).(\lambda (c4: C).(\lambda (H0: (csuba g c3 c4)).(\lambda (_: ((\forall 
 (e1: C).((clear c4 e1) \to (ex2 C (\lambda (e2: C).(csuba g e2 e1)) (\lambda 
-(e2: C).(clear c3 e2))))))).(\lambda (t: T).(\lambda (a: A).(\lambda (H2: 
-(arity g c3 t (asucc g a))).(\lambda (u: T).(\lambda (H3: (arity g c4 u 
+(e2: C).(clear c3 e2))))))).(\lambda (b: B).(\lambda (H2: (not (eq B b 
+Void))).(\lambda (u1: T).(\lambda (u2: T).(\lambda (e1: C).(\lambda (H3: 
+(clear (CHead c4 (Bind b) u2) e1)).(eq_ind_r C (CHead c4 (Bind b) u2) 
+(\lambda (c: C).(ex2 C (\lambda (e2: C).(csuba g e2 c)) (\lambda (e2: 
+C).(clear (CHead c3 (Bind Void) u1) e2)))) (ex_intro2 C (\lambda (e2: 
+C).(csuba g e2 (CHead c4 (Bind b) u2))) (\lambda (e2: C).(clear (CHead c3 
+(Bind Void) u1) e2)) (CHead c3 (Bind Void) u1) (csuba_void g c3 c4 H0 b H2 u1 
+u2) (clear_bind Void c3 u1)) e1 (clear_gen_bind b c4 e1 u2 H3)))))))))))) 
+(\lambda (c3: C).(\lambda (c4: C).(\lambda (H0: (csuba g c3 c4)).(\lambda (_: 
+((\forall (e1: C).((clear c4 e1) \to (ex2 C (\lambda (e2: C).(csuba g e2 e1)) 
+(\lambda (e2: C).(clear c3 e2))))))).(\lambda (t: T).(\lambda (a: A).(\lambda 
+(H2: (arity g c3 t (asucc g a))).(\lambda (u: T).(\lambda (H3: (arity g c4 u 
 a)).(\lambda (e1: C).(\lambda (H4: (clear (CHead c4 (Bind Abbr) u) 
 e1)).(eq_ind_r C (CHead c4 (Bind Abbr) u) (\lambda (c: C).(ex2 C (\lambda 
 (e2: C).(csuba g e2 c)) (\lambda (e2: C).(clear (CHead c3 (Bind Abst) t)