X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fclear%2Ffwd.ma;h=c0316133067cde403eff274368ed93692876cbce;hb=e92710b1d9774a6491122668c8463b8658114610;hp=4749583de34169306fa8edb969348f44b1acb924;hpb=831af787465e1bff886e22ee14b68c8f1bb0177c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/fwd.ma
index 4749583de..c03161330 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/fwd.ma
@@ -14,9 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/clear/fwd".
-
-include "clear/defs.ma".
+include "LambdaDelta-1/clear/defs.ma".
 
 theorem clear_gen_sort:
  \forall (x: C).(\forall (n: nat).((clear (CSort n) x) \to (\forall (P: 
@@ -117,21 +115,21 @@ theorem clear_gen_flat_r:
 \def
  \lambda (f: F).(\lambda (x: C).(\lambda (e: C).(\lambda (u: T).(\lambda (H: 
 (clear x (CHead e (Flat f) u))).(\lambda (P: Prop).(insert_eq C (CHead e 
-(Flat f) u) (\lambda (c: C).(clear x c)) P (\lambda (y: C).(\lambda (H0: 
-(clear x y)).(clear_ind (\lambda (_: C).(\lambda (c0: C).((eq C c0 (CHead e 
-(Flat f) u)) \to P))) (\lambda (b: B).(\lambda (e0: C).(\lambda (u0: 
-T).(\lambda (H1: (eq C (CHead e0 (Bind b) u0) (CHead e (Flat f) u))).(let H2 
-\def (eq_ind C (CHead e0 (Bind b) u0) (\lambda (ee: C).(match ee in C return 
-(\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | (CHead _ k _) 
-\Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind _) 
-\Rightarrow True | (Flat _) \Rightarrow False])])) I (CHead e (Flat f) u) H1) 
-in (False_ind P H2)))))) (\lambda (e0: C).(\lambda (c: C).(\lambda (H1: 
-(clear e0 c)).(\lambda (H2: (((eq C c (CHead e (Flat f) u)) \to P))).(\lambda 
-(_: F).(\lambda (_: T).(\lambda (H3: (eq C c (CHead e (Flat f) u))).(let H4 
-\def (eq_ind C c (\lambda (c0: C).((eq C c0 (CHead e (Flat f) u)) \to P)) H2 
-(CHead e (Flat f) u) H3) in (let H5 \def (eq_ind C c (\lambda (c0: C).(clear 
-e0 c0)) H1 (CHead e (Flat f) u) H3) in (H4 (refl_equal C (CHead e (Flat f) 
-u)))))))))))) x y H0))) H)))))).
+(Flat f) u) (\lambda (c: C).(clear x c)) (\lambda (_: C).P) (\lambda (y: 
+C).(\lambda (H0: (clear x y)).(clear_ind (\lambda (_: C).(\lambda (c0: 
+C).((eq C c0 (CHead e (Flat f) u)) \to P))) (\lambda (b: B).(\lambda (e0: 
+C).(\lambda (u0: T).(\lambda (H1: (eq C (CHead e0 (Bind b) u0) (CHead e (Flat 
+f) u))).(let H2 \def (eq_ind C (CHead e0 (Bind b) u0) (\lambda (ee: C).(match 
+ee in C return (\lambda (_: C).Prop) with [(CSort _) \Rightarrow False | 
+(CHead _ k _) \Rightarrow (match k in K return (\lambda (_: K).Prop) with 
+[(Bind _) \Rightarrow True | (Flat _) \Rightarrow False])])) I (CHead e (Flat 
+f) u) H1) in (False_ind P H2)))))) (\lambda (e0: C).(\lambda (c: C).(\lambda 
+(H1: (clear e0 c)).(\lambda (H2: (((eq C c (CHead e (Flat f) u)) \to 
+P))).(\lambda (_: F).(\lambda (_: T).(\lambda (H3: (eq C c (CHead e (Flat f) 
+u))).(let H4 \def (eq_ind C c (\lambda (c0: C).((eq C c0 (CHead e (Flat f) 
+u)) \to P)) H2 (CHead e (Flat f) u) H3) in (let H5 \def (eq_ind C c (\lambda 
+(c0: C).(clear e0 c0)) H1 (CHead e (Flat f) u) H3) in (H4 (refl_equal C 
+(CHead e (Flat f) u)))))))))))) x y H0))) H)))))).
 
 theorem clear_gen_all:
  \forall (c1: C).(\forall (c2: C).((clear c1 c2) \to (ex_3 B C T (\lambda (b: